Please use this identifier to cite or link to this item:

TitleExperimenting with predicate abstraction
Author(s)Miraldo, Victor Cacciari
Frade, M. J.
Lourenço, Cláudio
Pinto, Jorge Sousa
KeywordsFormal verification
Software model checking
Predicate abstraction
Issue date2013
CitationV. C. Miraldo, M. J. Frade, C. Lourenço, and J. S. Pinto. Experimenting with predicate abstraction. In B. S. Santos and J. Cachopo, editors, Proceedings of INForum’13 — Simpósio de Informática (SOFTPT track). Universidade de Évora, 2013.
Abstract(s)Predicate abstraction is a technique employed in software model checking to produce abstract models that can be conservatively checked for property violations in reasonable time. The precision degree of different abstractions of the same program may differ based on (i) the set of predicates used; or (ii) the algorithmic technique employed to gen- erate the model. In this paper we explain how we have implemented and optimized one such technique, that produces the most precise existential abstraction of a program, and give the first steps towards establishing a common framework for both this direct technique and a second one, based on cartesian abstraction by weakest precondition calculations.
AccessOpen access
Appears in Collections:HASLab - Resumos em livros de atas

Files in This Item:
File Description SizeFormat 
PredAbs-final.pdfDocumento principal345,91 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID