SMT-LIB
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Ground Interpolation for the Theory of Equality
- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study
- Race against the teens -- benchmarking mechanized math on pre-university problems
- Para-disagreement logics and their implementation through embedding in Coq and SMT
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- Editorial: Symbolic computation and satisfiability checking
- Algorithmic introduction of quantified cuts
- Faster, higher, stronger: E 2.3
- Heaps and Data Structures: A Challenge for Automated Provers
- Extending Sledgehammer with SMT solvers
- Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Verifying Whiley programs with Boogie
- Flexible proof production in an industrial-strength SMT solver
- Reasoning about vectors using an SMT theory of sequences
- MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions
- Optimization modulo non-linear arithmetic via incremental linearization
- An SMT solver for regular expressions and linear arithmetic over string length
- Vampire with a brain is a good ITP hammer
- Coming to terms with quantified reasoning
- EUFORIA: complete software model checking with uninterpreted functions
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Constraint programming for dynamic symbolic execution of JavaScript
- Scalable fine-grained proofs for formula processing
- Admissibility in Probabilistic Argumentation
- Applying machine learning to heuristics for real polynomial constraint solving
- Resolution proof transformation for compression and interpolation
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
- Proving termination of graph transformation systems using weighted type graphs over semirings
- Grez
- Building bridges between symbolic computation and satisfiability checking
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Automated Reasoning
- Modelling and solving temporal reasoning as propositional satisfiability
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Symbolic computation via program transformation
- Quantitative abstractions for collective adaptive systems
- Deciding probabilistic automata weak bisimulation: theory and practice
- Cylindrical algebraic decomposition with equational constraints
- The \textsc{SDEval} benchmarking toolkit
- Automated Termination in Model Checking Modulo Theories
- The incremental satisfiability problem for a two conjunctive normal form
- Validating QBF Validity in HOL4
- Deductive verification of floating-point Java programs in KeY
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- The 2013 evaluation of SMT-COMP and SMT-LIB
- Decision procedures for flat array properties
- An experiment with satisfiability modulo SAT
- Adding decision procedures to SMT solvers using axioms with triggers
- Semi-intelligible Isar proofs from machine-generated proofs
- Term Rewriting with Logical Constraints
- Using simplex method in verifying software safety
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
- Automated generation of exam sheets for automated deduction
- Linear time-dependent constraints programming with MSVL
- Matching multiplications in bit-vector formulas
- Combining decision procedures by (model-)equality propagation
- Exploiting step semantics for efficient bounded model checking of asynchronous systems
- SAT modulo linear arithmetic for solving polynomial constraints
- Horn clause solvers for program verification
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Polyhedral approximation of multivariate polynomials using Handelman's theorem
- TIP: tons of inductive problems
- Extensional crisis and proving identity
- Solving nonlinear integer arithmetic with MCSAT
- Randomized algorithms for finding the shortest negative cost cycle in networks
- The strategy challenge in SMT solving
- Certified roundoff error bounds using semidefinite programming
- An extension of lazy abstraction with interpolation for programs with arrays
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- LOIS: syntax and semantics
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
- Algorithmic reduction of biological networks with multiple time scales
- Improving ENIGMA-style clause selection while learning from history
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Witness runs for counter machines
- Layered clause selection for theory reasoning (short paper)
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Expressing polymorphic types in a many-sorted language
- Cutting the mix
- DRAT-based bit-vector proofs in CVC4
- Efficient representation of piecewise linear functions into Łukasiewicz logic modulo satisfiability
- On the complexity of reconstructing chemical reaction networks
- Computing small unsatisfiable cores in satisfiability modulo theories
- Petri Net Synthesis for Restricted Classes of Nets
- Optimization modulo the theory of floating-point numbers
- Fully incremental cylindrical algebraic decomposition
- Satisfiability modulo bounded checking
- Integrating external deduction tools with ACL2
- Solving quantified verification conditions using satisfiability modulo theories
- The TPTP typed first-order form with arithmetic
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
- Fast and Flexible Difference Constraint Propagation for DPLL(T)
This page was built for software: SMT-LIB
