Applying SAT methods in unbounded symbolic model checking

DOI10.1007/3-540-45657-0_19MaRDI QIDQ4804900zbMATH OpenFDO

Authors K. L. McMillan

Publication date 1 May 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/2404/24040250.htm

Mathematics Subject Classification ID

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

Recommendations

• Tuning SAT checkers for bounded model checking
• Model checking with Boolean Satisfiability
• A View from the Engine Room: Computational Support for Symbolic Model Checking
• Symbolic reachability analysis based on SAT-solvers
• Correct Hardware Design and Verification Methods

Cited in

(32)

• Partitioned PLTL model-checking for refined transition systems
• SAT and IP based algorithms for magic labeling including a complete search for total magic labelings
• A symbolic decision procedure for symbolic alternating finite automata
• How we designed winning algorithms for abstract argumentation and which insight we attained
• A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic
• Breaking symmetries in graph search with canonizing sets
• Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking
• Symbolic reachability analysis based on SAT-solvers
• Interpolant learning and reuse in SAT-based model checking
• Algorithms for Solving Satisfiability Problems with Qualitative Preferences
• Unbeast: Symbolic Bounded Synthesis
• SAT-Based Model Checking without Unrolling
• Linear completeness thresholds for bounded model checking
• Propositional SAT solving
• SAT-Based Model Checking
• Improvements to Hybrid Incremental SAT Algorithms
• Disjunctive closures for knowledge compilation
• scientific article; zbMATH DE number 2086590 (Why is no real title available?)
• Quantifier elimination by dependency sequents
• Computer Aided Verification
• Formal Methods for Hardware Verification
• Solving satisfiability problems with preferences
• Balanced covering arrays: A classification of covering arrays and packing arrays via exact methods
• Bisimulation conversion and verification procedure for goal-based control systems
• Partial quantifier elimination and property generation
• On enumerating short projected models
• On CNF conversion for SAT and SMT enumeration
• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
• Optimization techniques for Craig interpolant compaction in unbounded model checking
• Automatic symbolic compositional verification by learning assumptions
• Property-directed incremental invariant generation
• Efficient SAT-based bounded model checking for software verification

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: Applying SAT methods in unbounded symbolic model checking

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