2026-07-23T06:31:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4770 2024-03-06T10:29:40Z ddc:004 open_access

Predicate Abstraction in Program Verification: Survey and Current Trends Daniel, Jakub Parízek, Pavel program verification model checking predicate abstraction refinement 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jakub Daniel and Pavel Parízek 2014 Is Part Of OASIcs, Volume 43, 2014 Imperial College Computing Student Workshop InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.ICCSW.2014.27 urn:nbn:de:0030-drops-47706 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2014.27 eng https://creativecommons.org/licenses/by/3.0/legalcode