The following pages link to SIMPLIFY (Q17123):
Displaying 50 items.
- Decision procedures for flat array properties (Q287272) (← links)
- Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- Adding decision procedures to SMT solvers using axioms with triggers (Q287384) (← links)
- Proving properties of functional programs by equality saturation (Q300342) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- Decision procedures. An algorithmic point of view (Q518892) (← links)
- Automatic decidability and combinability (Q549666) (← links)
- Predicate abstraction in a program logic calculus (Q549686) (← links)
- Modular verification of multithreaded programs (Q557795) (← links)
- Structured derivations: a unified proof style for teaching mathematics (Q607406) (← links)
- Equality detection for linear arithmetic constraints (Q621462) (← links)
- Quantifier simplification by unification in SMT (Q831945) (← links)
- Product programs in the wild: retrofitting program verifiers to check information flow security (Q832225) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- Efficient weakest preconditions (Q835051) (← links)
- Combining nonstably infinite theories (Q851136) (← links)
- Formal verification of a C-like memory model and its uses for verifying program transformations (Q945054) (← links)
- Invariant based programming: Basic approach and teaching experiences (Q1019025) (← links)
- Don't care words with an application to the automata-based approach for real addition (Q1028730) (← links)
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (Q1037399) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- Theory decision by decomposition (Q1041591) (← links)
- Combination of convex theories: modularity, deduction completeness, and explanation (Q1041593) (← links)
- Automating regression verification of pointer programs by predicate abstraction (Q1650864) (← links)
- Solving quantified linear arithmetic by counterexample-guided instantiation (Q1688537) (← links)
- Counterexample-guided quantifier instantiation for synthesis in SMT (Q1702893) (← links)
- Automated verification of functional correctness of race-free GPU programs (Q1703009) (← links)
- Experience of improving the BLAST static verification tool (Q1758710) (← links)
- Generating error traces from verification-condition counterexamples (Q1776586) (← links)
- DCAS-based concurrent deques (Q1849584) (← links)
- Automatic software model checking via constraint logic (Q1887740) (← links)
- Solving bitvectors with MCSAT: explanations from bits and pieces (Q2096440) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- A learning-based approach to synthesizing invariants for incomplete verification engines (Q2208307) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- Refutation-based synthesis in SMT (Q2280222) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Unification with abstraction and theory instantiation in saturation-based reasoning (Q2324203) (← links)
- SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
- On interpolation in automated theorem proving (Q2352502) (← links)
- Verification of SpecC using predicate abstraction (Q2369884) (← links)
- The Daikon system for dynamic detection of likely invariants (Q2463543) (← links)
- Embedded software verification using symbolic execution and uninterpreted functions (Q2506297) (← links)
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification (Q2629858) (← links)
- Program verification with interacting analysis plugins (Q2642983) (← links)
