Simplify: a theorem prover for program checking
From MaRDI portal
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)- Don't care words with an application to the automata-based approach for real addition
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Solving quantified verification conditions using satisfiability modulo theories
- Theory decision by decomposition
- Combination of convex theories: modularity, deduction completeness, and explanation
- Lattice-based refinement in bounded model checking
- Automating regression verification of pointer programs by predicate abstraction
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Automated verification of functional correctness of race-free GPU programs
- SIMPLIFY
- Experience of improving the BLAST static verification tool
- Solving bitvectors with MCSAT: explanations from bits and pieces
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Verifying Whiley programs with Boogie
- A learning-based approach to synthesizing invariants for incomplete verification engines
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Syntax-guided quantifier instantiation
- Farkas-based tree interpolation
- Incremental search for conflict and unit instances of quantified formulas with E-matching
- Refutation-based synthesis in SMT
- Extending SMT solvers to higher-order logic
- SMELS: satisfiability modulo equality with lazy superposition
- On interpolation in automated theorem proving
- Verification of SpecC using predicate abstraction
- Embedded software verification using symbolic execution and uninterpreted functions
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Program verification with interacting analysis plugins
- Specification and verification challenges for sequential object-oriented programs
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Fault-tolerant aggregate signatures
- 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
- E-matching for fun and profit
- Model-based theory combination
- Programmed strategies for program verification
- 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
- Practical realisation and elimination of an ECC-related software bug attack
- Automating Induction with an SMT Solver
- Decision procedures for region logic
- Semantic subtyping with an SMT solver
- Adapting real quantifier elimination methods for conflict set computation
- Modular verification of procedure equivalence in the presence of memory allocation
- Proving properties of functional programs by equality saturation
- Correct code containing containers
- Roles, stacks, histories: a triple for Hoare
- Satisfiability solving and model generation for quantified first-order logic formulas
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- Modular SMT proofs for fast reflexive checking inside Coq
- SAT-Based Model Checking
- Satisfiability modulo theories
- Bounded quantifier instantiation for checking inductive invariants
- Counterexample-Guided Model Synthesis
- Congruence closure with free variables
- scientific article; zbMATH DE number 3880145 (Why is no real title available?)
- Search-space partitioning for parallelizing SMT solvers
- Inductive prover based on equality saturation for a lazy functional language
- Verifying Heap-Manipulating Programs in an SMT Framework
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Efficient Well-Definedness Checking
- Engineering DPLL(T) + Saturation
- Certification Using the Mobius Base Logic
- Predicate Abstraction in a Program Logic Calculus
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
- Abstract Counterexamples for Non-disjunctive Abstractions
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- 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
- Constraint solving for finite model finding in SMT solvers
- Verification conditions for source-level imperative programs
- Towards modularly comparing programs using automated theorem provers
- The mechanical verification of a DPLL-based satisfiability solver
- Automatic decidability and combinability
- Predicate abstraction in a program logic calculus
- Modular verification of multithreaded programs
- Bugs, moles and skeletons: symbolic reasoning for software development
- Structured derivations: a unified proof style for teaching mathematics
- Embedded domain specific verifiers
- Verification of SMT systems with quantifiers
- Synthesizing history and prophecy variables for symbolic model checking
- Equality detection for linear arithmetic constraints
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Fast approximations of quantifier elimination
- Early verification of legal compliance via bounded satisfiability checking
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- Invariant checking for SMT-based systems with quantifiers
- Transforming optimization problems into disciplined convex programming form
- Solving hard Mizar problems with instantiation and strategy invention
- Invariant neural architecture for learning term synthesis in instantiation proving
- A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
- SMT and functional equation solving over the reals: challenges from the IMO
- Machine learning for quantifier selection in cvc5
- The QSMA algorithm for quantifiers in SMT
- A formal model to prove instantiation termination for E-matching-based axiomatisations
- Reasoning about Hilbert's choice operator in SMT
- Quantifier simplification by unification in SMT
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)
