Predicate Abstraction in Program Verification: Survey and Current Trends
Identifikátory výsledku
Kód výsledku v 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>
Výsledek na webu
<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>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Predicate Abstraction in Program Verification: Survey and Current Trends
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Predicate Abstraction in Program Verification: Survey and Current Trends
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GA14-11384S" target="_blank" >GA14-11384S: Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2014
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Imperial College Computing Student Workshop 2014
ISBN
978-3-939897-76-7
ISSN
2190-6807
e-ISSN
—
Počet stran výsledku
9
Strana od-do
27-35
Název nakladatele
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Místo vydání
Dagstuhl, Germany
Místo konání akce
London, UK
Datum konání akce
25. 9. 2014
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—