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

DOI10.1007/S10703-009-0081-1MaRDI QIDQ845244zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Computer Aided Verification
• Symbolic model checking with rich assertional languages
• Verifying specifications in the language L against temporal properties nonexpressible in this language
• Symbolic model checking: \(10^{20}\) states and beyond
• scientific article; zbMATH DE number 910719

Cites work

• scientific article; zbMATH DE number 1670768 (Why is no real title available?)
• scientific article; zbMATH DE number 1701756 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 1948389 (Why is no real title available?)
• scientific article; zbMATH DE number 2080036 (Why is no real title available?)
• scientific article; zbMATH DE number 2084712 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• Bounded model checking of infinite state systems
• Computer Aided Verification
• Computer Aided Verification
• Constraint-based verification of parameterized cache coherence protocols
• Efficient Symbolic Representations for Arithmetic Constraints in Verification
• HyTech: A model checker for hybrid systems
• Learning to verify branching time properties
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(6)

• Computer Aided Verification
• Program specialization for verifying infinite state systems: an experimental evaluation
• Combining Predicate Abstraction with Fixpoint Approximations
• Generalization strategies for the verification of infinite state systems
• Proving VLRL action properties with the Maude model checker
• Partial predicate abstraction and counter-example guided refinement

Describes a project that uses

Uses Software

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

This page was built for publication: Action language verifier: An infinite-state model checker for reactive software specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q845244)