CVC

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