SIMPLIFY

swMATH4976MaRDI QIDQ17123FDOQ17123

Author name not available (Why is that?)

Described by source

• Simplify: a theorem prover for program checking

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
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Theoretical Aspects of Computing – ICTAC 2005
• 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
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Certifying optimality of state estimation programs.
• 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
• Congruence closure with free variables
• Proving properties of functional programs by equality saturation
• Automatic decidability and combinability
• Solving bitvectors with MCSAT: explanations from bits and pieces
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• 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
• isl: An integer set library for the polyhedral model
• 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
• Bugs, moles and skeletons: symbolic reasoning for software development
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• Correct code containing containers
• Valigator: A Verification Tool with Bound and Invariant Generation
• Satisfiability modulo theories
• Descriptive and Relative Completeness of Logics for Higher-Order Functions
• Back to the future, revisiting precise program verification using SMT solvers
• Tools and Algorithms for the Construction and Analysis of Systems
• Invariant based programming: Basic approach and teaching experiences
• The mechanical verification of a DPLL-based satisfiability solver
• 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
• One logic to use them all
• 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
• Dafny: an automatic program verifier for functional correctness
• Theorem proving using lazy proof explication.
• 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
• ${\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
• Adapting real quantifier elimination methods for conflict set computation
• Modular verification of procedure equivalence in the presence of memory allocation
• 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
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• Automating theorem proving with SMT
• Two for the price of one: lifting separation logic assertions
• Programmed strategies for program verification
• Extended static checking
• Formal proof of SCHUR conjugate function
• Synthesis of positive logic programs for checking a class of definitions with infinite quantification
• Search-space partitioning for parallelizing SMT solvers
• Automatic software model checking via constraint logic
• OpenSMT2: an SMT solver for multi-core and cloud computing
• SMELS: satisfiability modulo equality with lazy superposition

This page was built for software: SIMPLIFY