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

DOI10.1007/S10703-009-0081-1zbMATH Open1185.68427OpenAlexW2010729520MaRDI QIDQ845244FDOQ845244

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

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

zbMATH Keywords

Automated abstractionInfinite state model checkingKeywords: Symbolic model checking

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (6)

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

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)