Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results.
Tevfik BultanRichard GerberWilliam PughPublished in: ACM Trans. Program. Lang. Syst. (1999)
Keyphrases
- concurrent systems
- model checking
- temporal logic
- process algebra
- transition systems
- formal specification
- symbolic model checking
- symbolic representation
- distributed systems
- finite state
- verification method
- formal verification
- model checker
- asynchronous circuits
- web services composition
- search algorithm
- dynamic programming