swMATH9449MaRDI QIDQ21432FDOQ21432
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007/978-3-540-70545-1_28
Cited In (98)
- AXDInterpolator
- DyverseRBT
- URBiVA: uniform reduction to bit-vector arithmetic
- Being careful about theory combination
- Automated reasoning in \(\mathcal{ALCQ}\) via SMT
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
- Local abstraction refinement for probabilistic timed programs
- Processes and continuous change in a SAT-based planner
- Symbolic Execution as DPLL Modulo Theories
- Sharing is caring: combination of theories
- 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
- Aalta
- FACT
- SMT-based scenario verification for hybrid systems
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Fast congruence closure and extensions
- Stochastic local search for SMT: combining theory solvers with WalkSAT
- Leviathan
- 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
- Optimization modulo theories with linear rational costs
- Formal modelling, analysis and verification of hybrid systems
- Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming
- An alternative to SAT-based approaches for bit-vectors
- Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
- Whale: an interpolation-based algorithm for inter-procedural verification
- Interpolant Generation for UTVPI
- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
- 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
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Verifying industrial hybrid systems with \textsc{MathSAT}
- Efficiently solving quantified bit-vector formulas
- Boolector
- QOCA
- Yices
- MATISSE
- BPEL2PN
- Eclat
- Ptolemy
- CVC Lite
- KRATOS
- RunLim
- SYMBA
- CVC
- Cleaneling
- NuSMV3
- Memorax
- URBiVA
- YASM
- HyDI
- Equality detection for linear arithmetic constraints
- CalCS
- Capo
- fzn2smt
- Wolverine
- RATSY
- ICS
- nuXmv
- ManyOpt
- CyPhySim
- SAPA
- ABsolver
- Zapato
- OptiMathSAT
- AO4BPEL
- PRISM-PSY
- STP
- 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
- Cassowary
- Papyrus-RT
- 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
- Integration of an LP solver into interval constraint propagation
- Exact Incremental Analysis of Timed Automata with an SMT-Solver
- Advanced SMT techniques for weighted model integration
- Planning as satisfiability: heuristics
- MedleySolver
- Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
- Complexity of fixed-size bit-vector logics
- Model-based theory combination
- Structured learning modulo theories
- From under-approximations to over-approximations and back
- The MathSAT5 SMT solver
- Title not available (Why is that?)
- MedleySolver: online SMT algorithm selection
- OCRA
- 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
- Interpolation-based GR(1) assumptions refinement
This page was built for software: MathSAT
