Simplify: a theorem prover for program checking
From MaRDI portal
Publication:3546294
DOI10.1145/1066100.1066102zbMATH Open1323.68462OpenAlexW2055477538MaRDI QIDQ3546294FDOQ3546294
Authors: David L. Detlefs, Greg Nelson, James B. Saxe 
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
Recommendations
- scientific article; zbMATH DE number 1696761
- Proof simplification and automated theorem proving
- Programming a symbolic model checker in a fully expansive theorem prover
- A Progressive Simplifier for Satisfiability Modulo Theories
- A simple test improves checking satisfiability
- Computer Aided Verification
- scientific article; zbMATH DE number 3880145
- scientific article; zbMATH DE number 3963223
Cited In (only showing first 100 items - show all)
- A learning-based approach to synthesizing invariants for incomplete verification engines
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Verifying Whiley programs with Boogie
- Adapting real quantifier elimination methods for conflict set computation
- Abstract Counterexamples for Non-disjunctive Abstractions
- Farkas-based tree interpolation
- Syntax-guided quantifier instantiation
- Incremental search for conflict and unit instances of quantified formulas with E-matching
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Inductive prover based on equality saturation for a lazy functional language
- SMELS: satisfiability modulo equality with lazy superposition
- Synthesizing history and prophecy variables for symbolic model checking
- Program verification with interacting analysis plugins
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- Modular SMT proofs for fast reflexive checking inside Coq
- Roles, stacks, histories: a triple for Hoare
- Solving quantified bit-vector formulas using binary decision diagrams
- SAT-Based Model Checking
- Invariant checking for SMT-based systems with quantifiers
- Embedded software verification using symbolic execution and uninterpreted functions
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Solving hard Mizar problems with instantiation and strategy invention
- Transforming optimization problems into disciplined convex programming form
- Invariant neural architecture for learning term synthesis in instantiation proving
- A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
- Embedded domain specific verifiers
- Counterexample-Guided Model Synthesis
- Fast approximations of quantifier elimination
- Early verification of legal compliance via bounded satisfiability checking
- Semantic subtyping with an SMT solver
- Constraint solving for finite model finding in SMT solvers
- Verifying Heap-Manipulating Programs in an SMT Framework
- Quantifier simplification by unification in SMT
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Efficient weakest preconditions
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Modular verification of procedure equivalence in the presence of memory allocation
- Towards modularly comparing programs using automated theorem provers
- Automating Induction with an SMT Solver
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Predicate abstraction in a program logic calculus
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Programmed strategies for program verification
- Automated verification of functional correctness of race-free GPU programs
- Fault-tolerant aggregate signatures
- Lattice-based refinement in bounded model checking
- Decision procedures for flat array properties
- Interpolation systems for ground proofs in automated deduction: a survey
- Adding decision procedures to SMT solvers using axioms with triggers
- Semantically-guided goal-sensitive reasoning: model representation
- An instantiation scheme for satisfiability modulo theories
- Bounded quantifier instantiation for checking inductive invariants
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- On deciding satisfiability by theorem proving with speculative inferences
- Search-space partitioning for parallelizing SMT solvers
- Congruence closure with free variables
- Proving properties of functional programs by equality saturation
- OpenSMT2: an SMT solver for multi-core and cloud computing
- Automatic decidability and combinability
- Experience of improving the BLAST static verification tool
- Solving bitvectors with MCSAT: explanations from bits and pieces
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Combining nonstably infinite theories
- Refutation-based synthesis in SMT
- Solving quantified verification conditions using satisfiability modulo theories
- Theory decision by decomposition
- Structured derivations: a unified proof style for teaching mathematics
- Don't care words with an application to the automata-based approach for real addition
- Automating regression verification of pointer programs by predicate abstraction
- SIMPLIFY
- Verification conditions for source-level imperative programs
- Equality detection for linear arithmetic constraints
- Congruence closure in intensional type theory
- Bugs, moles and skeletons: symbolic reasoning for software development
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- Correct code containing containers
- Satisfiability modulo theories
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Decision procedures for region logic
- Combination of convex theories: modularity, deduction completeness, and explanation
- The mechanical verification of a DPLL-based satisfiability solver
- Modular verification of multithreaded programs
- Title not available (Why is that?)
- Extending SMT solvers to higher-order logic
- On interpolation in automated theorem proving
- Theory exploration powered by deductive synthesis
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Specification and verification challenges for sequential object-oriented programs
- Certification Using the Mobius Base Logic
- Practical realisation and elimination of an ECC-related software bug attack
- Model-based theory combination
- Predicate Abstraction in a Program Logic Calculus
- E-matching for fun and profit
- Satisfiability solving and model generation for quantified first-order logic formulas
- Verification of SMT systems with quantifiers
- Verification of SpecC using predicate abstraction
- Efficient Well-Definedness Checking
- Engineering DPLL(T) + Saturation
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
Uses Software
This page was built for publication: Simplify: a theorem prover for program checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3546294)
