MathSAT
From MaRDI portal
Software:21432
swMATH9449MaRDI QIDQ21432FDOQ21432
Author name not available (Why is that?)
Cited In (55)
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
- Automated Reasoning in $\mathcal{ALCQ}$ via SMT
- Sharing Is Caring: Combination of Theories
- SMT-based scenario verification for hybrid systems
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Fast congruence closure and extensions
- Being careful about theory combination
- Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming
- From Under-Approximations to Over-Approximations and Back
- Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
- Local abstraction refinement for probabilistic timed programs
- Interpolant Generation for UTVPI
- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
- Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
- Interpolation-Based GR(1) Assumptions Refinement
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Verifying industrial hybrid systems with \textsc{MathSAT}
- Processes and continuous change in a SAT-based planner
- Integration of an LP Solver into Interval Constraint Propagation
- Formal Modelling, Analysis and Verification of Hybrid Systems
- Optimization Modulo Theories with Linear Rational Costs
- Symbolic Execution as DPLL Modulo Theories
- Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT
- Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
- Efficiently solving quantified bit-vector formulas
- An Alternative to SAT-Based Approaches for Bit-Vectors
- Equality detection for linear arithmetic constraints
- The MathSAT5 SMT Solver
- Quantifier-free encoding of invariants for hybrid systems
- SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Solving constraint satisfaction problems with SAT modulo theories
- Monitoring and recovery for web service applications
- Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results
- Strategies for scalable symbolic execution-driven test generation for programs
- Simulating circuit-level simplifications on CNF
- HySAT: An efficient proof engine for bounded model checking of hybrid systems
- Exact Incremental Analysis of Timed Automata with an SMT-Solver
- A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
- Boosting Lazy Abstraction for SystemC with Partial Order Reduction
- Costs and rewards in priced timed automata
- Advanced SMT techniques for weighted model integration
- Planning as satisfiability: heuristics
- Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
- Complexity of fixed-size bit-vector logics
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- Model-based theory combination
- URBiVA: Uniform Reduction to Bit-Vector Arithmetic
- Structured learning modulo theories
- Title not available (Why is that?)
- MedleySolver: online SMT algorithm selection
- 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
This page was built for software: MathSAT
