JetBrains Research — наука, меняющая мир

Семинар: Достижимость, направляемая свойством


В докладе рассматривается подход к символьной верификации помеченных систем переходов. Вместо раскрутки отношения перехода он инкременально генерирует леммы, которые индуктивны относительно пошаговых приближений достижимых состояний. Таким образом, алгоритм постепенно уточняет свойство, рано или поздно строя либо индуктивное усиление свойства, либо контрпример к свойству безопасности.


21.10.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 2