Pith. sign in

REVIEW

Satisfiability Modulo ODEs

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1310.8278 v1 pith:R63HFCIV submitted 2013-10-30 cs.LO cs.SYeess.SY

Sicun Gao , Soonho Kong , Edmund Clarke This is my paper
classification cs.LOcs.SYeess.SY
keywords algorithmsformulasodesvariablesbenchmarkscontainingdelta-completedemonstrate
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

We study SMT problems over the reals containing ordinary differential equations. They are important for formal verification of realistic hybrid systems and embedded software. We develop delta-complete algorithms for SMT formulas that are purely existentially quantified, as well as exists-forall formulas whose universal quantification is restricted to the time variables. We demonstrate scalability of the algorithms, as implemented in our open-source solver dReal, on SMT benchmarks with several hundred nonlinear ODEs and variables.

Discussion (0). Sign in to comment.

Pith tools