Computer Aided Verification

DOI10.1007/B98490MaRDI QIDQ5312909zbMATH OpenOpenAlexFDO

Authors Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman

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

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1979549
• scientific article; zbMATH DE number 1979550
• Interpolating quantifier-free Presburger arithmetic
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• Interpolant based decision procedure for quantifier-free Presburger arithmetic

Cited in

(11)

• Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem
• Efficient theory combination via Boolean search
• scientific article; zbMATH DE number 1979549 (Why is no real title available?)
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• TaPAS: The Talence Presburger Arithmetic Suite
• Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
• An approach for extracting a small unsatisfiable core
• SAT-Based Model Checking
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
• Interpolant based decision procedure for quantifier-free Presburger arithmetic
• A sound and complete abstraction for reasoning about parallel prefix sums

Describes a project that uses

Uses Software

• OPBDP
• TLA

This page was built for publication: Computer Aided Verification

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