Formal Verification of Software Designs in Hierarchical State Transition Matrix with SMT-based Bounded Model Checking.
Weiqiang KongNoriyuki KatahiraMasahiko WatanabeTetsuro KatayamaKenji HisazumiAkira FukudaPublished in: APSEC (2011)
Keyphrases
- formal verification
- bounded model checking
- model checking
- transition matrix
- program slicing
- automated verification
- model checker
- symbolic model checking
- temporal logic
- markov chain
- finite state
- software development
- linear temporal logic
- multi agent systems
- state space
- learning algorithm
- formal specification
- multi agent