License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.ICCSW.2014.27
URN: urn:nbn:de:0030-drops-47706
URL: https://drops.dagstuhl.de/opus/volltexte/2014/4770/
Go to the corresponding OASIcs Volume Portal


Daniel, Jakub ; ParĂ­zek, Pavel

Predicate Abstraction in Program Verification: Survey and Current Trends

pdf-format:
7.pdf (0.5 MB)


Abstract

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.

BibTeX - Entry

@InProceedings{daniel_et_al:OASIcs:2014:4770,
  author =	{Jakub Daniel and Pavel Par{\'i}zek},
  title =	{{Predicate Abstraction in Program Verification: Survey and Current Trends}},
  booktitle =	{2014 Imperial College Computing Student Workshop},
  pages =	{27--35},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-76-7},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{43},
  editor =	{Rumyana Neykova and Nicholas Ng},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4770},
  URN =		{urn:nbn:de:0030-drops-47706},
  doi =		{10.4230/OASIcs.ICCSW.2014.27},
  annote =	{Keywords: program verification, model checking, predicate abstraction, refinement}
}

Keywords: program verification, model checking, predicate abstraction, refinement
Collection: 2014 Imperial College Computing Student Workshop
Issue Date: 2014
Date of publication: 08.10.2014


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI