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