Семинары
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Календарь
Поиск
Регистрация семинара

RSS
Ближайшие семинары




Российский гибридный семинар STEP-2023 по фундаментальным вопросам программной инженерии теории и экспериментальному программированию
8 марта 2024 г. 14:00–15:30, г. Новосибирск, Институт систем информатики им. А. П. Ершова
 




[Automated Reasoning with Continuous Data]

М. В. Коровина

Количество просмотров:
Эта страница:103



Аннотация: Семинар 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
 
  Обратная связь:
 Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024