SMT-LIB
From MaRDI portal
Software:16290
swMATH4103MaRDI QIDQ16290FDOQ16290
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Extending Sledgehammer with SMT solvers
- Faster, higher, stronger: E 2.3
- Algorithmic introduction of quantified cuts
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions
- EUFORIA: complete software model checking with uninterpreted functions
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- 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
- Resolution proof transformation for compression and interpolation
- Automated Reasoning
- Modelling and solving temporal reasoning as propositional satisfiability
- Deciding probabilistic automata weak bisimulation: theory and practice
- Automated Termination in Model Checking Modulo Theories
- Term Rewriting with Logical Constraints
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Beagle – A Hierarchic Superposition Theorem Prover
- SMTtoTPTP – A Converter for Theorem Proving Formats
- 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
- 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
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- An extension of lazy abstraction with interpolation for programs with arrays
- Cutting the mix
- Computing small unsatisfiable cores in satisfiability modulo theories
- Integrating external deduction tools with ACL2
- Solving quantified verification conditions using satisfiability modulo theories
- Fast and Flexible Difference Constraint Propagation for DPLL(T)
- bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR
- dReal: An SMT Solver for Nonlinear Theories over the Reals
- Efficiently solving quantified bit-vector formulas
- Title not available (Why is that?)
- Light-Weight SMT-based Model Checking
- Natural domain SMT: a preliminary assessment
- Automated testing and debugging of SAT and QBF solvers
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- HYST
- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
- Loop Analysis by Quantification over Iterations
- Solving constraint satisfaction problems with SAT modulo theories
- A decision procedure for separation logic in SMT
- Z3str2: an efficient solver for strings, regular expressions, and length constraints
- Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
- Strategies for scalable symbolic execution-driven test generation for programs
- Exact Incremental Analysis of Timed Automata with an SMT-Solver
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- CoReS: a tool for computing core graphs via SAT/SMT solvers
- CoReS: a tool for computing core graphs via SAT/SMT solvers
- Extending SMT solvers to higher-order logic
- Extending Sledgehammer with SMT solvers
- A decision procedure for (co)datatypes in SMT solvers
- SMT proof checking using a logical framework
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
- Complexity of fixed-size bit-vector logics
- Partitioned Memory Models for Program Analysis
- Integer induction in saturation
- A Survey of Satisfiability Modulo Theory
- Definability of Accelerated Relations in a Theory of Arrays and Its Applications
- E-matching for fun and profit
- Computer Aided Verification
- Ground interpolation for the theory of equality
- Playing in the grey area of proofs
- Dafny: an automatic program verifier for functional correctness
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Automatic proof and disproof in Isabelle/HOL
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Polynomial constraints and unsat cores in \textsc{Tarski}
- Thousands of geometric problems for geometric theorem provers (TGTP)
- Satisfiability Modulo Theories
- Conflict Resolution
- A system for solving constraint satisfaction problems with SMT
- Computing all-pairs shortest paths by leveraging low treewidth
- Solving strong controllability of temporal problems with uncertainty using SMT
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
- Ground Interpolation for the Theory of Equality
- Editorial: Symbolic computation and satisfiability checking
- Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving
- Coming to terms with quantified reasoning
- Speeding up quantified bit-vector SMT solvers by bit-width reductions and extensions
- Scalable fine-grained proofs for formula processing
- 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
- Model Finding for Recursive Functions in SMT
- TIP: Tools for Inductive Provers
- $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation
- Building bridges between symbolic computation and satisfiability checking
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Title not available (Why is that?)
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Symbolic computation via program transformation
- Cylindrical algebraic decomposition with equational constraints
This page was built for software: SMT-LIB