MathSAT
From MaRDI portal
Software:21432
No author found.
Related Items (55)
Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ From Under-Approximations to Over-Approximations and Back ⋮ 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 ⋮ Unnamed Item ⋮ Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) ⋮ Strategies for scalable symbolic execution-driven test generation for programs ⋮ Simulating circuit-level simplifications on CNF ⋮ Planning as satisfiability: heuristics ⋮ The MathSAT5 SMT Solver ⋮ Fast congruence closure and extensions ⋮ HySAT: An efficient proof engine for bounded model checking of hybrid systems ⋮ A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL ⋮ Optimization Modulo Theories with Linear Rational Costs ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers ⋮ Equality detection for linear arithmetic constraints ⋮ Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces ⋮ Efficiently solving quantified bit-vector formulas ⋮ SMT-based scenario verification for hybrid systems ⋮ Being careful about theory combination ⋮ Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results ⋮ Symbolic Execution as DPLL Modulo Theories ⋮ SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems ⋮ Local abstraction refinement for probabilistic timed programs ⋮ SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata ⋮ Quantifier-free encoding of invariants for hybrid systems ⋮ Processes and continuous change in a SAT-based planner ⋮ Solving constraint satisfaction problems with SAT modulo theories ⋮ Monitoring and recovery for web service applications ⋮ Boosting Lazy Abstraction for SystemC with Partial Order Reduction ⋮ Interpolation-Based GR(1) Assumptions Refinement ⋮ An Alternative to SAT-Based Approaches for Bit-Vectors ⋮ Complexity of fixed-size bit-vector logics ⋮ Structured learning modulo theories ⋮ Unnamed Item ⋮ Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems ⋮ Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis ⋮ URBiVA: Uniform Reduction to Bit-Vector Arithmetic ⋮ Engineering constraint solvers for automatic analysis of probabilistic hybrid automata ⋮ 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 ⋮ Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions ⋮ Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints ⋮ Costs and rewards in priced timed automata ⋮ Advanced SMT techniques for weighted model integration ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Solving strong controllability of temporal problems with uncertainty using SMT ⋮ Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties ⋮ Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming ⋮ Model-based Theory Combination ⋮ MedleySolver: online SMT algorithm selection
This page was built for software: MathSAT
