SAT Modulo Differential Equation Simulations

Kód výsledku v 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>

Nalezeny alternativní kódy

RIV/68407700:21240/20:00341733

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

SAT Modulo Differential Equation Simulations

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

SAT Modulo Differential Equation Simulations

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2020

Kód důvěrnosti údajů

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

Název statě ve sborníku

Tests and Proofs

ISBN

978-3-030-50994-1

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

20

Strana od-do

80-99

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Bergen

Datum konání akce

22. 6. 2020

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—