SMT-LIB

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