Proving more properties with bounded model checking

DOI10.1007/978-3-540-27813-9_8MaRDI QIDQ5312948zbMATH OpenOpenAlexFDO

Authors Mohammad Awedh, Fabio Somenzi

Publication date 25 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b98490

Mathematics Subject Classification ID

Temporal logic (03B44) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Termination criteria for bounded model checking: extensions and comparison
• Verification, Model Checking, and Abstract Interpretation
• Incremental and complete bounded model checking for full PLTL
• Accelerating bounded model checking of safety properties
• Bounded model checking for all regular properties

Cited in

(7)

• Linear completeness thresholds for bounded model checking
• SAT-Based Model Checking
• Complete SAT-Based Model Checking for Context-Free Processes
• Formalizing bounded increase
• Incremental and complete bounded model checking for full PLTL
• Convergence testing in term-level bounded model checking
• Verification, Model Checking, and Abstract Interpretation

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: Proving more properties with bounded model checking

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