The following pages link to SIMPLIFY (Q17123):
Displaying 50 items.
- Specification and verification challenges for sequential object-oriented programs (Q2643131) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- (Q2767989) (← links)
- Congruence Closure in Intensional Type Theory (Q2817913) (← links)
- Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams (Q2818019) (← links)
- OpenSMT2: An SMT Solver for Multi-core and Cloud Computing (Q2818042) (← links)
- E-matching for Fun and Profit (Q2864401) (← links)
- Model-based Theory Combination (Q2864402) (← links)
- Programmed Strategies for Program Verification (Q2864527) (← links)
- Ground interpolation for the theory of equality (Q2881073) (← links)
- Practical Realisation and Elimination of an ECC-Related Software Bug Attack (Q2890003) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- Decision Procedures for Region Logic (Q2891431) (← links)
- Two for the Price of One: Lifting Separation Logic Assertions (Q2914243) (← links)
- (Q2963876) (← links)
- Adapting Real Quantifier Elimination Methods for Conflict Set Computation (Q2964460) (← links)
- Modular Verification of Procedure Equivalence in the Presence of Memory Allocation (Q2988675) (← links)
- Correct Code Containing Containers (Q3012966) (← links)
- Dafny: An Automatic Program Verifier for Functional Correctness (Q3066108) (← links)
- Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas (Q3067537) (← links)
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Q3075472) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- A Lightweight Approach for Loop Summarization (Q3172925) (← links)
- SAT-Based Model Checking (Q3176368) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- (Q3181652) (← links)
- Back to the future (Q3189836) (← links)
- Bounded Quantifier Instantiation for Checking Inductive Invariants (Q3303891) (← links)
- Counterexample-Guided Model Synthesis (Q3303898) (← links)
- Congruence Closure with Free Variables (Q3303931) (← links)
- Search-Space Partitioning for Parallelizing SMT Solvers (Q3453241) (← links)
- Verifying Heap-Manipulating Programs in an SMT Framework (Q3510799) (← links)
- Thread Quantification for Concurrent Shape Analysis (Q3512507) (← links)
- SMELS: Satisfiability Modulo Equality with Lazy Superposition (Q3540073) (← links)
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier (Q3543656) (← links)
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding (Q3557085) (← links)
- Formal Proof of SCHUR Conjugate Function (Q3582705) (← links)
- Descriptive and Relative Completeness of Logics for Higher-Order Functions (Q3591433) (← links)
- Certification Using the Mobius Base Logic (Q3602993) (← links)
- Predicate Abstraction in a Program Logic Calculus (Q3605465) (← links)
- ${\mathcal{T}}$ -Decision by Decomposition (Q3608774) (← links)
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints (Q3617770) (← links)
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories (Q3636870) (← links)
- Incremental Instance Generation in Local Reasoning (Q3636873) (← links)
- Abstract Counterexamples for Non-disjunctive Abstractions (Q3646262) (← links)
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme (Q3655207) (← links)
- (Q4531754) (← links)
- Constraint solving for finite model finding in SMT solvers (Q4593094) (← links)
- (Q4809071) (← links)
- One Logic to Use Them All (Q4928425) (← links)
