scientific article; zbMATH DE number 1903346

zbMath1010.68522MaRDI QIDQ4804887

Sanjit A. Seshia, Randal E. Bryant, Shuvendu K. Lahiri

Publication date: 1 May 2003

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

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

Related Items

Modeling for Verification, Satisfiability Modulo Theories, Fast congruence closure and extensions, A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures, Local Search For Satisfiability Modulo Integer Arithmetic Theories, Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic, Algorithms for computing minimal unsatisfiable subsets of constraints, What’s Decidable About Program Verification Modulo Axioms?, Building small equality graphs for deciding equality logic with uninterpreted functions, Zero, successor and equality in BDDs, Variant-Based Satisfiability in Initial Algebras, Embedded software verification using symbolic execution and uninterpreted functions, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, Satisfiability Procedures for Combination of Theories Sharing Integer Offsets, Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker, Word level bitwidth reduction for unbounded hardware model checking, Data compression for proof replay, Theory decision by decomposition, Parameterised Boolean equation systems, The small model property: How small can it be?, MedleySolver: online SMT algorithm selection

Uses Software

• PVS
• HOL
• Chaff
• Velev SAT Benchmarks