DROPS

Document

DOI: 10.4230/OASIcs.ICCSW.2014.27

Predicate Abstraction in Program Verification: Survey and Current Trends

Authors: Jakub Daniel and Pavel Parízek

Published in: OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop

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.

Cite as

Jakub Daniel and Pavel Parízek. Predicate Abstraction in Program Verification: Survey and Current Trends. In 2014 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 43, pp. 27-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

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

Search Results

Documents authored by Daniel, Jakub

Predicate Abstraction in Program Verification: Survey and Current Trends

Abstract

Cite as

Thanks for your feedback!

Could not send message