Počet záznamů: 1
SAT Modulo Differential Equation Simulations
- 1.
SYSNO ASEP 0531242 Druh ASEP C - Konferenční příspěvek (mezinárodní konf.) Zařazení RIV D - Článek ve sborníku Název SAT Modulo Differential Equation Simulations Tvůrce(i) Kolárik, T. (CZ)
Ratschan, Stefan (UIVT-O) SAI, RID, ORCIDZdroj.dok. Tests and Proofs. - Cham : Springer, 2020 / Ahrendt W. ; Wehrheim H. - ISSN 0302-9743 - ISBN 978-3-030-50994-1 Rozsah stran s. 80-99 Poč.str. 20 s. Forma vydání Tištěná - P Akce TAP 2020: The International Conference on Tests and Proofs /14./ Datum konání 22.06.2020 - 23.06.2020 Místo konání Bergen Země NO - Norsko Typ akce WRD Jazyk dok. eng - angličtina Země vyd. CH - Švýcarsko Klíč. slova constraint solving ; Boolean satisfiability ; formal verification Vědní obor RIV IN - Informatika Obor OECD Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8) Institucionální podpora UIVT-O - RVO:67985807 EID SCOPUS 85087276051 DOI 10.1007/978-3-030-50995-8_5 Anotace 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. Pracoviště Ústav informatiky Kontakt Tereza Šírová, sirova@cs.cas.cz, Tel.: 266 053 800 Rok sběru 2021
Počet záznamů: 1