SIMPLIFY
From MaRDI portal
Software:17123
swMATH4976MaRDI QIDQ17123FDOQ17123
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Verifying Heap-Manipulating Programs in an SMT Framework
- Title not available (Why is that?)
- The Daikon system for dynamic detection of likely invariants
- Quantifier simplification by unification in SMT
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Programming Languages and Systems
- Programming Languages and Systems
- Efficient weakest preconditions
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Automating Induction with an SMT Solver
- Computer Aided Verification
- Computer Aided Verification
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Theoretical Aspects of Computing – ICTAC 2005
- Dafny: An Automatic Program Verifier for Functional Correctness
- Predicate abstraction in a program logic calculus
- Automated verification of functional correctness of race-free GPU programs
- Counterexample-guided quantifier instantiation for synthesis in SMT
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- 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
- New results on rewrite-based satisfiability procedures
- isl: An Integer Set Library for the Polyhedral Model
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- An instantiation scheme for satisfiability modulo theories
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- On deciding satisfiability by theorem proving with speculative inferences
- Proving properties of functional programs by equality saturation
- Automatic decidability and combinability
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
- The Mechanical Verification of a DPLL-Based Satisfiability Solver
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- One Logic to Use Them All
- Thread Quantification for Concurrent Shape Analysis
- Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Verification conditions for source-level imperative programs
- Lazy abstraction
- Equality detection for linear arithmetic constraints
- Computer Aided Verification
- Bounded Quantifier Instantiation for Checking Inductive Invariants
- Congruence Closure with Free Variables
- Valigator: A Verification Tool with Bound and Invariant Generation
- Descriptive and Relative Completeness of Logics for Higher-Order Functions
- Tools and Algorithms for the Construction and Analysis of Systems
- Invariant based programming: Basic approach and teaching experiences
- Modular verification of multithreaded programs
- Extending SMT solvers to higher-order logic
- On interpolation in automated theorem proving
- Theory exploration powered by deductive synthesis
- Computer Aided Verification
- Specification and verification challenges for sequential object-oriented programs
- Certification Using the Mobius Base Logic
- Model-based theory combination
- Frontiers of Combining Systems
- Predicate Abstraction in a Program Logic Calculus
- E-matching for fun and profit
- Ground interpolation for the theory of equality
- Correct Code Containing Containers
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
- Satisfiability Modulo Theories
- Tools and Algorithms for the Construction and Analysis of Systems
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Decision procedures. An algorithmic point of view
- A Lightweight Approach for Loop Summarization
- Back to the future
- ${\mathcal{T}}$ -Decision by Decomposition
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Using History Invariants to Verify Observers
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Verifying Whiley programs with Boogie
- Practical Realisation and Elimination of an ECC-Related Software Bug Attack
- Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas
- Incremental Instance Generation in Local Reasoning
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Algebraic Methodology and Software Technology
- Abstract Counterexamples for Non-disjunctive Abstractions
- Title not available (Why is that?)
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Two for the price of one: lifting separation logic assertions
- Programmed strategies for program verification
- Extended static checking
- Verifying and Synthesizing Software with Recursive Functions
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- Automatic software model checking via constraint logic
- SMELS: satisfiability modulo equality with lazy superposition
- Experience of improving the BLAST static verification tool
- Zap: Automated Theorem Proving for Software Analysis
This page was built for software: SIMPLIFY
