cvc3

swMATH4886MaRDI QIDQ17038FDOQ17038

Author name not available (Why is that?)

Official website: http://www.cs.nyu.edu/acsys/cvc3/

Cited In (only showing first 100 items - show all)

• Title not available (Why is that?)
• Extending Sledgehammer with SMT solvers
• Minimal counterexamples for linear-time probabilistic verification
• Towards Automatic Stability Analysis for Rely-Guarantee Proofs
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• An experiment with satisfiability modulo SAT
• Rewriting Induction + Linear Arithmetic = Decision Procedure
• New results on rewrite-based satisfiability procedures
• Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
• SAT modulo linear arithmetic for solving polynomial constraints
• The complexity of reversal-bounded model-checking
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• Expressing polymorphic types in a many-sorted language
• Lazy satisfiability modulo theories
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Computing small unsatisfiable cores in satisfiability modulo theories
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• Solving quantified verification conditions using satisfiability modulo theories
• A formal semantics of extended hierarchical state transition matrices using CSP\#
• Don't care words with an application to the automata-based approach for real addition
• Behavioral interface specification languages
• A unified framework for DPLL(T) + certificates
• Efficiently solving quantified bit-vector formulas
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• GNT
• HOL-Boogie
• ACSL
• SMT-LIB
• Caduceus
• Why3
• Yices
• Alt-Ergo
• Gappa
• ISP
• UCLID
• SIMPLIFY
• TASS_
• z3
• COMICS
• GiNaCRA
• FADAlib
• Zap
• ESC4
• TaPAS
• Title not available (Why is that?)
• Collective assertions
• Verification conditions for source-level imperative programs
• CVC Lite
• CLSAT
• Interproc
• CVC
• MathSAT
• DiPro
• HighSpec
• CVT
• VeriCool
• Monotonox
• CSIsat
• MUP
• Jahob
• RSat
• I-RiSC
• Combining theories with shared set operations
• Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
• LASH
• LIRA
• H-PILoT
• KLEE-FP
• Nemerle
• Robbins Conjecture
• STP
• Satisfiability modulo theories
• Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
• Challenges in Satisfiability Modulo Theories
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Extending Sledgehammer with SMT solvers
• SMT proof checking using a logical framework
• Multi-prover verification of floating-point programs
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• Model-based theory combination
• E-matching for fun and profit
• Satisfiability solving and model generation for quantified first-order logic formulas
• Dafny: an automatic program verifier for functional correctness
• Automatic proof and disproof in Isabelle/HOL
• Conflict Resolution
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• TASS: the toolkit for accurate scientific software
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• Heaps and Data Structures: A Challenge for Automated Provers
• Verifying Whiley programs with Boogie
• Being careful about theory combination
• checkbashisms
• Formal analysis of the compact position reporting algorithm
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Automating theorem proving with SMT
• Volume Computation for Boolean Combination of Linear Arithmetic Constraints
• Formal proof of SCHUR conjugate function
• The strategy challenge in SMT solving

This page was built for software: cvc3