More effective interpolations in software model checking

An approach to CEGAR-based model checking which has proved to be successful on large models employs Craig interpolation to efficiently construct parsimonious abstractions. Following this design, we introduce new applications, universal safety interpolant and existential error interpolant, of Craig i...

Бүрэн тодорхойлолт

Номзүйн дэлгэрэнгүй
Үндсэн зохиолчид: Tian, C, Duan, Z, Ong, C
Формат: Conference item
Хэвлэсэн: Association for Computing Machinery 2017