Cited in
(only showing first 100 items - show all)- Symbolic Execution as DPLL Modulo Theories
- AXDInterpolator
- DyverseRBT
- Processes and continuous change in a SAT-based planner
- Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
- An alternative to SAT-based approaches for bit-vectors
- Automated reasoning in \(\mathcal{ALCQ}\) via SMT
- Leviathan
- A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
- Advanced SMT techniques for weighted model integration
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- URBiVA: uniform reduction to bit-vector arithmetic
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
- Boosting Lazy Abstraction for SystemC with Partial Order Reduction
- Local abstraction refinement for probabilistic timed programs
- Costs and rewards in priced timed automata
- Sharing is caring: combination of theories
- Aalta
- Being careful about theory combination
- FACT
- MedleySolver: online SMT algorithm selection
- Interpolation-based GR(1) assumptions refinement
- Whale: an interpolation-based algorithm for inter-procedural verification
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- The MathSAT5 SMT solver
- Stochastic local search for SMT: combining theory solvers with WalkSAT
- Efficiently solving quantified bit-vector formulas
- Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
- Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
- Model-based theory combination
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
- Equality detection for linear arithmetic constraints
- Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems
- Solving constraint satisfaction problems with SAT modulo theories
- Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
- Strategies for scalable symbolic execution-driven test generation for programs
- Planning as satisfiability: heuristics
- Simulating circuit-level simplifications on CNF
- Beaver
- Boolector
- QOCA
- WSAT
- BarcelogicTools
- HySAT
- UBCSAT
- TASS
- PHAVer
- Yices
- MATISSE
- BPEL2PN
- Eclat
- Ptolemy
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Fast congruence closure and extensions
- CVC Lite
- KRATOS
- RunLim
- SYMBA
- CVC
- Cleaneling
- NuSMV3
- Memorax
- URBiVA
- YASM
- HyDI
- CalCS
- Capo
- fzn2smt
- Wolverine
- RATSY
- Optimization modulo theories with linear rational costs
- Formal modelling, analysis and verification of hybrid systems
- HySAT: An efficient proof engine for bounded model checking of hybrid systems
- ICS
- nuXmv
- ManyOpt
- CyPhySim
- SAPA
- ABsolver
- Zapato
- OptiMathSAT
- AO4BPEL
- PRISM-PSY
- STP
- Cassowary
- Papyrus-RT
- Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming
- Integration of an LP solver into interval constraint propagation
- scientific article; zbMATH DE number 7178358 (Why is no real title available?)
- MedleySolver
- Interpolant Generation for UTVPI
- Complexity of fixed-size bit-vector logics
- Monitoring and recovery for web service applications
- Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results
- Structured learning modulo theories
- Verifying industrial hybrid systems with \textsc{MathSAT}
- Exact Incremental Analysis of Timed Automata with an SMT-Solver
- SMT-based scenario verification for hybrid systems
This page was built for software: MathSAT
