swMATH9462MaRDI QIDQ21445FDOQ21445
Author name not available (Why is that?)
Official website: http://verify.stanford.edu/CVC/
Cited In (62)
- Formal Approaches to Software Testing
- Title not available (Why is that?)
- Computer Aided Verification
- Optimization modulo non-linear arithmetic via incremental linearization
- Preface to the special issue ``SI: satisfiability modulo theories
- Generalizing DPLL and satisfiability for equalities
- Term Rewriting and Applications
- Computer Aided Verification
- Correct Hardware Design and Verification Methods
- Mining propositional simplification proofs for small validating clauses
- New results on rewrite-based satisfiability procedures
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- The SAT-based approach to separation logic
- Strategies for combining decision procedures
- Combining nonstably infinite theories
- A framework for satisfiability modulo theories
- Combining non-stably infinite theories
- Building small equality graphs for deciding equality logic with uninterpreted functions
- kcnfs
- Model Checking Software
- BarcelogicTools
- ARGO-LIB
- TVOC
- UCLID
- Zap
- ComFoRT
- CVC Lite
- MathSAT
- CVT
- MOPS
- MUP
- Equality detection for linear arithmetic constraints
- RSat
- EVC
- MicroRogue
- An approach for extracting a small unsatisfiable core
- ICS
- TSAT++
- EVES
- Embedded software verification using symbolic execution and uninterpreted functions
- A Decision Procedure for Bit-Vectors and Arrays
- Model Checking Software
- Automated Deduction – CADE-19
- Producing proofs from an arithmetic decision procedure in elliptical LF
- Title not available (Why is that?)
- \textsf{TSAT++}: an open platform for satisfiability modulo theories
- Computer Aided Verification
- Automated Technology for Verification and Analysis
- Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli
- Title not available (Why is that?)
- Logics in Artificial Intelligence
- Frontiers of Combining Systems
- Rewrite-based decision procedures
- Enhancing Program Verification with Lemmas
- Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs
- Title not available (Why is that?)
- Translation and run-time validation of loop transformations
- Combining equational reasoning
- Imperative LF meta-programming
- Computer Science Logic
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
This page was built for software: CVC
