|
|
Российский гибридный семинар STEP-2023 по фундаментальным вопросам программной инженерии
теории и экспериментальному программированию
8 марта 2024 г. 14:00–15:30, г. Новосибирск, Институт систем информатики им. А. П. Ершова
|
 |
|
 |
|
|
|
[Automated Reasoning with Continuous Data]
М. В. Коровина |
| Количество просмотров: |
| Эта страница: | 65 |
|
Аннотация:
Семинар STEP-2024 продолжает традицию специальных заседаний в Международный женский день.
Аннотация доклада: In this talk we report on ongoing research on solving non-linear constraints over the reals occurring in a wide range of applications, starting with program verification, ranging over verification of real-world designs all the way to automation of formally verified proofs of mathematical statements.
In our framework methods from Computable Analysis and Automated Reasoning are combined to meet efficiency and expressiveness. This approach is applicable to a large number of constraints involving computable non-linear functions, piecewise polynomial splines, transcendental functions and solutions of polynomial differential equations.
We give an introduction to the ksmt calculus for checking satisfiability of non-linear constraints in a CDCL style way inspired by advances in SAT solving. Along proof search ksmt resolves two types of conflicts: linear and non-linear. Linear conflicts are delegated to a decision procedure for linear real arithmetic and non-linear conflicts are resolved by local linearisations separating the solution set and the current conflict. We show that the ksmt calculus is a σ-complete decision procedure for bounded problems.
Запись выступления есть на YouTube: https://youtu.be/L0IT0RXrKcI
Язык доклада: английский
Website:
https://youtu.be/L0IT0RXrKcI
|
|
Обратная связь: