Action language verifier: An infinite-state model checker for reactive software specifications

DOI10.1007/s10703-009-0081-1zbMath1185.68427OpenAlexW2010729520MaRDI QIDQ845244

Tuba Yavuz-Kahveci, Tevfik Bultan

Publication date: 5 February 2010

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-009-0081-1

zbMATH Keywords

Automated abstractionInfinite state model checkingKeywords: Symbolic model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Generalization strategies for the verification of infinite state systems ⋮ Combining Predicate Abstraction with Fixpoint Approximations ⋮ Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation ⋮ Partial predicate abstraction and counter-example guided refinement

Uses Software

• SPIN
• HyTech
• NuSMV
• Uppaal
• MONA
• LEVER

Cites Work

• HyTech: A model checker for hybrid systems
• Constraint-based verification of parameterized cache coherence protocols
• Bounded model checking of infinite state systems
• Learning to verify branching time properties
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Efficient Symbolic Representations for Arithmetic Constraints in Verification
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item