AG
дык формализация реал арифметики
Size: a a a
2021 June 08
Oℕ
да, кому она нужна
AG
гибридным системщикам
Oℕ
те, кто физику какую-то будут доказывать?
AG
щас довольно остромодная тема для верификации
AG
> Examples of CPS include smart grid, autonomous automobile systems, medical monitoring, industrial control systems, robotics systems, and automatic pilot avionics.
AG
я ж как раз про это начал в сторону поездов посты писать
Oℕ
и им точно нужна действительнозначная математика?
AG
надо кстати добить эту серию на неделе
AG
им нужно верифицировать штуки, работающие с аппроксимациями
Oℕ
и нужны непрерынвые поля для этого?
AG
ну там вот такими штуками занимаются https://lfcps.org/pub/VeriPhy.pdf
AG
> The standard semantics of dL feature arithmetic on real numbers, which are crucial for physics but ill-suited to efficient execution. Next, we soundly approximate the real semantics with a computable 32-bit integer interval arithmetic semantics, enabling efficient sandbox execution. Here, we present our translation to interval arithmetic and prove it sound in Isabelle/HOL.