SAT Modulo Differential Equation Simulations

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F20%3A00531242" target="_blank" >RIV/67985807:_____/20:00531242 - isvavai.cz</a>

Alternative codes found

RIV/68407700:21240/20:00341733

Result on the web

<a href="http://dx.doi.org/10.1007/978-3-030-50995-8_5" target="_blank" >http://dx.doi.org/10.1007/978-3-030-50995-8_5</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-50995-8_5" target="_blank" >10.1007/978-3-030-50995-8_5</a>

Result language

angličtina

Original language name

SAT Modulo Differential Equation Simulations

Original language description

Differential equations are of immense importance for modeling physical phenomena, often in combination with discrete modeling formalisms. In current industrial practice, properties of the resulting models are checked by testing, using simulation tools. Research on SAT solvers that are able to handle differential equations has aimed at replacing tests by correctness proofs. However, there are fundamental limitations to such approaches in the form of undecidability, and moreover, the resulting solvers do not scale to problems of the size commonly handled by simulation tools. Also, in many applications, classical mathematical semantics of differential equations often does not correspond well to the actual intended semantics, and hence a correctness proof wrt. mathematical semantics does not ensure correctness of the intended system. In this paper, we head at overcoming those limitations by an alternative approach to handling differential equations within SAT solvers. This approach is usually based on the semantics used by tests in simulation tools, but still may result in mathematically precise correctness proofs wrt. that semantics. Experiments with a prototype implementation confirm the promise of such an approach.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2020

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Tests and Proofs

ISBN

978-3-030-50994-1

ISSN

0302-9743

e-ISSN

—

Number of pages

20

Pages from-to

80-99

Publisher name

Springer

Place of publication

Cham

Event location

Bergen

Event date

Jun 22, 2020

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—