A fixpoint based encoding for bounded model checking

DOI10.1007/3-540-36126-X_15MaRDI QIDQ4427907zbMATH OpenFDO

Authors Alan M. Frisch, Daniel Sheridan, Toby Walsh

Publication date 14 September 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2517/25170238.htm

Mathematics Subject Classification ID

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

Recommendations

• Linear Encodings of Bounded LTL Model Checking
• Computable fixpoints in well-structured symbolic model checking
• Bounded model checking using satisfiability solving
• Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
• Theory and Applications of Satisfiability Testing
• A compact linear translation for bounded model checking
• Lattice-based refinement in bounded model checking

Cited in

(9)

• Incremental bounded model checking for embedded software
• Computable fixpoints in well-structured symbolic model checking
• Counterexample-preserving reduction for symbolic model checking
• A compact linear translation for bounded model checking
• Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Comparing SAT encodings for model checking
• On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
• Computer Science Logic

Describes a project that uses

Uses Software

• SMART_
• Chaff

This page was built for publication: A fixpoint based encoding for bounded model checking

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