The following pages link to SMT-LIB (Q16290):
Displaying 50 items.
- Deciding probabilistic automata weak bisimulation: theory and practice (Q282105) (← links)
- The 2013 evaluation of SMT-COMP and SMT-LIB (Q286784) (← links)
- Decision procedures for flat array properties (Q287272) (← links)
- An experiment with satisfiability modulo SAT (Q287334) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Adding decision procedures to SMT solvers using axioms with triggers (Q287384) (← links)
- Strategies for scalable symbolic execution-driven test generation for programs (Q350939) (← links)
- Algorithmic introduction of quantified cuts (Q402115) (← links)
- Combining decision procedures by (model-)equality propagation (Q436376) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- Exploiting step semantics for efficient bounded model checking of asynchronous systems (Q436411) (← links)
- SAT modulo linear arithmetic for solving polynomial constraints (Q438576) (← links)
- Resolution proof transformation for compression and interpolation (Q479815) (← links)
- An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
- Solving constraint satisfaction problems with SAT modulo theories (Q487632) (← links)
- Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories (Q487655) (← links)
- Complexity of fixed-size bit-vector logics (Q504997) (← links)
- Decision procedures. An algorithmic point of view (Q518892) (← links)
- Exploiting subproblem optimization in SAT-based maxsat algorithms (Q525063) (← links)
- Z3str2: an efficient solver for strings, regular expressions, and length constraints (Q526767) (← links)
- Vampire with a brain is a good ITP hammer (Q831938) (← links)
- Optimization modulo non-linear arithmetic via incremental linearization (Q831943) (← links)
- An SMT solver for regular expressions and linear arithmetic over string length (Q832270) (← links)
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) (Q861691) (← links)
- Design and results of the Fifth Answer Set Programming Competition (Q899444) (← links)
- Integrating external deduction tools with ACL2 (Q1006728) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- Symbolic computation via program transformation (Q1623144) (← links)
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition (Q1656596) (← links)
- Polynomial constraints and unsat cores in \textsc{Tarski} (Q1662298) (← links)
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (Q1687709) (← links)
- Solving quantified linear arithmetic by counterexample-guided instantiation (Q1688537) (← links)
- Randomized algorithms for finding the shortest negative cost cycle in networks (Q1693163) (← links)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574) (← links)
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers (Q1697332) (← links)
- Cutting the mix (Q1702886) (← links)
- The incremental satisfiability problem for a two conjunctive normal form (Q1744433) (← links)
- Tactics and certificates in Meta Dedukti (Q1791152) (← links)
- Positive solutions of systems of signed parametric polynomial inequalities (Q1798326) (← links)
- A generic framework for implicate generation modulo theories (Q1799090) (← links)
- Superposition with datatypes and codatatypes (Q1799098) (← links)
- A FOOLish encoding of the next state relations of imperative programs (Q1799102) (← links)
- Datatypes with shared selectors (Q1799121) (← links)
- A decision procedure for separation logic in SMT (Q1990511) (← links)
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings (Q1996869) (← links)
- Sharpening constraint programming approaches for bit-vector theory (Q2011567) (← links)
- Linear time-dependent constraints programming with MSVL (Q2015809) (← links)
- Algorithmic reduction of biological networks with multiple time scales (Q2051597) (← links)
- Integer induction in saturation (Q2055871) (← links)
- Superposition with first-class booleans and inprocessing clausification (Q2055873) (← links)
