Simplify: a theorem prover for program checking
From MaRDI portal
Publication:3546294
DOI10.1145/1066100.1066102zbMath1323.68462OpenAlexW2055477538MaRDI QIDQ3546294
David L. Detlefs, James B. Saxe, Greg Nelson
Publication date: 21 December 2008
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1066100.1066102
Related Items
Practical Realisation and Elimination of an ECC-Related Software Bug Attack, Automating Induction with an SMT Solver, Decision Procedures for Region Logic, Decision procedures for flat array properties, Interpolation systems for ground proofs in automated deduction: a survey, Semantically-guided goal-sensitive reasoning: model representation, Adding decision procedures to SMT solvers using axioms with triggers, Quantifier simplification by unification in SMT, Product programs in the wild: retrofitting program verifiers to check information flow security, Theory exploration powered by deductive synthesis, Verification of SpecC using predicate abstraction, Efficient weakest preconditions, Lattice-based refinement in bounded model checking, Proving properties of functional programs by equality saturation, Synthesis of positive logic programs for checking a class of definitions with infinite quantification, Search-Space Partitioning for Parallelizing SMT Solvers, SAT-Based Model Checking, Satisfiability Modulo Theories, Inductive Prover Based on Equality Saturation for a Lazy Functional Language, Combining nonstably infinite theories, Semantic subtyping with an SMT solver, Program verification with interacting analysis plugins, Specification and verification challenges for sequential object-oriented programs, Automating regression verification of pointer programs by predicate abstraction, HOL-Boogie -- an interactive prover-backend for the verifying C compiler, Structured derivations: a unified proof style for teaching mathematics, Solving quantified linear arithmetic by counterexample-guided instantiation, Constraint solving for finite model finding in SMT solvers, Equality detection for linear arithmetic constraints, Embedded domain specific verifiers, Verifying Heap-Manipulating Programs in an SMT Framework, Verification of SMT systems with quantifiers, Synthesizing history and prophecy variables for symbolic model checking, Adapting Real Quantifier Elimination Methods for Conflict Set Computation, Automated verification of functional correctness of race-free GPU programs, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, On deciding satisfiability by theorem proving with speculative inferences, An instantiation scheme for satisfiability modulo theories, A learning-based approach to synthesizing invariants for incomplete verification engines, First-order automated reasoning with theories: when deduction modulo theory meets practice, Verification conditions for source-level imperative programs, Modular Verification of Procedure Equivalence in the Presence of Memory Allocation, SMELS: Satisfiability Modulo Equality with Lazy Superposition, Efficient Well-Definedness Checking, Engineering DPLL(T) + Saturation, Syntax-guided quantifier instantiation, Farkas-based tree interpolation, Incremental search for conflict and unit instances of quantified formulas with E-matching, Bounded Quantifier Instantiation for Checking Inductive Invariants, Counterexample-Guided Model Synthesis, Congruence Closure with Free Variables, Formal verification of a C-like memory model and its uses for verifying program transformations, Correct Code Containing Containers, Roles, stacks, histories: A triple for Hoare, Experience of improving the BLAST static verification tool, Automatic decidability and combinability, Predicate abstraction in a program logic calculus, The Mechanical Verification of a DPLL-Based Satisfiability Solver, Modular verification of multithreaded programs, Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development, Certification Using the Mobius Base Logic, Predicate Abstraction in a Program Logic Calculus, Refutation-based synthesis in SMT, Embedded software verification using symbolic execution and uninterpreted functions, Fault-Tolerant Aggregate Signatures, Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas, Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Congruence Closure in Intensional Type Theory, Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams, OpenSMT2: An SMT Solver for Multi-core and Cloud Computing, Extending SMT solvers to higher-order logic, SIMPLIFY, Don't care words with an application to the automata-based approach for real addition, Abstract Counterexamples for Non-disjunctive Abstractions, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis, Solving quantified verification conditions using satisfiability modulo theories, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Theory decision by decomposition, Combination of convex theories: modularity, deduction completeness, and explanation, Solving bitvectors with MCSAT: explanations from bits and pieces, E-matching for Fun and Profit, Model-based Theory Combination, Programmed Strategies for Program Verification, A posthumous contribution by Larry Wos: excerpts from an unpublished column, Verifying Whiley programs with Boogie, SMELS: satisfiability modulo equality with lazy superposition, On interpolation in automated theorem proving
Uses Software
