Можем ли мы разработать правила вывода логики разделения в Z3 и использовать ее для автоматической проверки некоторых реквизитов?

Question

Можем ли мы разработать правила вывода логики разделения в Z3 и использовать ее для автоматической проверки некоторых реквизитов?

Можем ли мы разработать правила вывода и аксиомы о логике разделения в z3 и использовать ее для автоматической проверки некоторых реквизитов? Например," x=y /\ (x |-> z) |- x=y /\ (y |-> z)"

2

coq z3 hoare-logic

Источник

user1999320 15 май '14 в 13:51

1 ответ

Другие вопросы по тегам coq z3 hoare-logic

user869966 21 май '14 в 12:54 2014-05-21 12:54 · Answer 1 · 2014-05-21 12:54

Возможно. Несколько групп работают над средствами проверки логики разделения на основе решателей SMT или интегрированы с ними. Вот несколько недавних публикаций на эту тему:

Ruzica Piskac, Thomas Wies, Damien Zufferey: Автоматизация логики разделения с помощью SMT. CAV 2013

Матко Ботинкан, Мэтью Дж. Паркинсон, Вольфрам Шульте: верификация логики разделения программ на языке C с помощью SMT Solver. Электр. Отмечает Теор. Вычи. Sci. 254

Хуан Антонио Наварро Перес, Андрей Рыбальченко: Логика разделения Теории по модулю. APLAS 2013

Я уверен, что есть много других SL-пруверов, но я знаю, что у меня в голове есть SLAyer.