CVC: A cooperating validity checker

DOI10.1007/3-540-45657-0_40MaRDI QIDQ4804919zbMATH OpenFDO

Authors Aaron Stump, Clark Barrett, David L. Dill

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/24040500.htm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• Computer Aided Verification
• VCS: a verifier for component-based systems
• Recent Trends in Algebraic Development Techniques
• Valigator: A Verification Tool with Bound and Invariant Generation

Cited in

(28)

• An approach for extracting a small unsatisfiable core
• A framework for satisfiability modulo theories
• CVC
• A decision procedure for (co)datatypes in SMT solvers
• Strategies for combining decision procedures
• Preface to the special issue ``SI: satisfiability modulo theories
• Building small equality graphs for deciding equality logic with uninterpreted functions
• Embedded software verification using symbolic execution and uninterpreted functions
• Generalizing DPLL and satisfiability for equalities
• Validated proof-producing decision procedures
• Rewrite-based decision procedures
• Imperative LF meta-programming
• A decision procedure for (co)datatypes in SMT solvers
• A Brief Overview of PVS
• Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
• Combining equational reasoning
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• An online proof-producing decision procedure for mixed-integer linear arithmetic
• Combining non-stably infinite theories
• Computer Aided Verification
• Computer Aided Verification
• A Decision Procedure for Bit-Vectors and Arrays
• Equality detection for linear arithmetic constraints
• Translation and run-time validation of loop transformations
• Optimization modulo non-linear arithmetic via incremental linearization
• Combining nonstably infinite theories
• Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
• The SAT-based approach to separation logic

Describes a project that uses

Uses Software

• Chaff
• PVS

This page was built for publication: CVC: A cooperating validity checker

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