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

TitleExperimenting with Predicate Abstraction
Author(s)Miraldo, Victor Cacciari
KeywordsProgram verification
Predicate abstraction
Issue dateJan-2014
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 generate the model. In this report we explain how we have extended the implementation of one such technique, that produces the most precise ex- istential abstraction of a program, and we establish a common framework for both this direct technique and a second one, based on cartesian ab- straction by weakest precondition calculations. This report a product of the research grant BI22012 PTDC/EIA-CCO/117590/2010 UMINHO, in the scope of the AVIACC project, supervised by Professors Jorge Sousa Pinto and Maria João Frade.
AccessOpen access
Appears in Collections:HASLab - Relatórios técnicos

Files in This Item:
File Description SizeFormat 
VMiraldo-report.pdfRelatório379,04 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