Семинар по синхронизации дизъюнктов Хорна и неограниченной верификации

Семинар по синхронизации дизъюнктов Хорна и неограниченной верификации

В докладе будет освящено применение решателей дизъюнктов Хорна к анализу программного кода. В первой части вкратце будут рассмотрены некоторые проблемы в современном состоянии области верификации ПО и описан сравнительно недавно предложенный подход к автоматической неограниченной верификации программного кода. Будут обсуждаться способы кодирования программ в системы дизъюнктов Хорна и некоторые подходы к их решению.

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

Докладчик: Дмитрий Мордвинов.

10.04.2017, 17:15.

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