scientific article; zbMATH DE number 1979554

MaRDI QIDQ4427907zbMATH OpenFDO

Authors Alan M. Frisch, Daniel Sheridan, Toby Walsh

Publication date 14 September 2003

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
• scientific article; zbMATH DE number 2084774 (Why is no real title available?)
• 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:

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