Predicate Abstraction in Program Verification: Survey and Current Trends
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F14%3A10279710" target="_blank" >RIV/00216208:11320/14:10279710 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.4230/OASIcs.ICCSW.2014.27" target="_blank" >http://dx.doi.org/10.4230/OASIcs.ICCSW.2014.27</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4230/OASIcs.ICCSW.2014.27" target="_blank" >10.4230/OASIcs.ICCSW.2014.27</a>
Alternative languages
Result language
angličtina
Original language name
Predicate Abstraction in Program Verification: Survey and Current Trends
Original language description
A popular approach to verification of software system correctness is model checking. To achieve scalability needed for large systems, model checking has to be augmented with abstraction. In this paper, we provide an overview of selected techniques of program verification based on predicate abstraction. We focus on techniques that advanced the state-of-the-art in a significant way, including counterexample-guided abstraction refinement, lazy abstraction, and current trends in the form of extensions targeting, for example, data structures and multi-threading. We discuss limitations of these techniques and present our plans for addressing some of them.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GA14-11384S" target="_blank" >GA14-11384S: Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2014
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Imperial College Computing Student Workshop 2014
ISBN
978-3-939897-76-7
ISSN
2190-6807
e-ISSN
—
Number of pages
9
Pages from-to
27-35
Publisher name
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place of publication
Dagstuhl, Germany
Event location
London, UK
Event date
Sep 25, 2014
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—