δ-Complete Decision Procedures for Satisfiability over the Reals
From MaRDI portal
Publication:2908499
DOI10.1007/978-3-642-31365-3_23zbMath1358.03028arXiv1204.3513OpenAlexW1496681274MaRDI QIDQ2908499
Jeremy Avigad, Sicun Gao, Edmund M. Clarke
Publication date: 5 September 2012
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1204.3513
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items (21)
A heuristic prover for real inequalities ⋮ Computing compositional proofs of input-to-output stability using SOS optimization and \(\delta\)-decidability ⋮ Hybrid Multirate PALS ⋮ Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration ⋮ Deciding first-order formulas involving univariate mixed trigonometric-polynomials ⋮ The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans ⋮ Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test ⋮ Counterexample-guided computation of polyhedral Lyapunov functions for piecewise linear systems ⋮ \textsf{symQV}: automated symbolic verification of quantum programs ⋮ Complete and tractable machine-independent characterizations of second-order polytime ⋮ Relating syntactic and semantic perturbations of hybrid automata ⋮ A search-based procedure for nonlinear real arithmetic ⋮ Quasi-decidability of a fragment of the first-order theory of real numbers ⋮ Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration ⋮ Automated and formal synthesis of neural barrier certificates for dynamical models ⋮ Numerically-aided deductive safety proof for a powertrain control system ⋮ The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ Compositional construction of control barrier functions for continuous-time stochastic hybrid systems ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey ⋮ Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
Uses Software
This page was built for publication: δ-Complete Decision Procedures for Satisfiability over the Reals
