SIMPLIFY
From MaRDI portal
Software:17123
No author found.
Related Items (only showing first 100 items - show all)
Ground interpolation for the theory of equality ⋮ 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 ⋮ Automatic software model checking via constraint logic ⋮ Proving properties of functional programs by equality saturation ⋮ A Lightweight Approach for Loop Summarization ⋮ 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 ⋮ Combining nonstably infinite theories ⋮ Two for the Price of One: Lifting Separation Logic Assertions ⋮ Program verification with interacting analysis plugins ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Automating regression verification of pointer programs by predicate abstraction ⋮ Back to the future ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Structured derivations: a unified proof style for teaching mathematics ⋮ Unnamed Item ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Constraint solving for finite model finding in SMT solvers ⋮ Equality detection for linear arithmetic constraints ⋮ Verifying Heap-Manipulating Programs in an SMT Framework ⋮ Thread Quantification for Concurrent Shape Analysis ⋮ Adapting Real Quantifier Elimination Methods for Conflict Set Computation ⋮ Counterexample-guided quantifier instantiation for synthesis in SMT ⋮ 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 ⋮ HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier ⋮ Bounded Quantifier Instantiation for Checking Inductive Invariants ⋮ Counterexample-Guided Model Synthesis ⋮ Congruence Closure with Free Variables ⋮ The Daikon system for dynamic detection of likely invariants ⋮ A Polymorphic Intermediate Verification Language: Design and Logical Encoding ⋮ Formal verification of a C-like memory model and its uses for verifying program transformations ⋮ Correct Code Containing Containers ⋮ Decision procedures. An algorithmic point of view ⋮ Unnamed Item ⋮ Experience of improving the BLAST static verification tool ⋮ Unnamed Item ⋮ Formal Proof of SCHUR Conjugate Function ⋮ One Logic to Use Them All ⋮ Automatic decidability and combinability ⋮ Predicate abstraction in a program logic calculus ⋮ Modular verification of multithreaded programs ⋮ Descriptive and Relative Completeness of Logics for Higher-Order Functions ⋮ Generating error traces from verification-condition counterexamples ⋮ 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 ⋮ ${\mathcal{T}}$ -Decision by Decomposition ⋮ Dafny: An Automatic Program Verifier for Functional Correctness ⋮ 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 ⋮ Unnamed Item ⋮ 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 ⋮ Invariant based programming: Basic approach and teaching experiences ⋮ Extending SMT solvers to higher-order logic ⋮ Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories ⋮ Incremental Instance Generation in Local Reasoning ⋮ 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 ⋮ Unification with abstraction and theory instantiation in saturation-based reasoning ⋮ Theory decision by decomposition ⋮ Combination of convex theories: modularity, deduction completeness, and explanation ⋮ DCAS-based concurrent deques ⋮ 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 ⋮ Unnamed Item
This page was built for software: SIMPLIFY