2026-08-16T06:48:57Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:701 2024-03-06T10:28:21Z ddc:004 open_access

Explaining Data Type Reduction in the Shape Analysis Framework Wachter, Björn Canonical abstraction data type reduction model checking parameterized system infinite-state Automatic formal verification of systems composed of a large or even unbounded number of components is difficult as the state space of these systems is prohibitively large. Abstraction techniques automatically construct finite approximations of infinite-state systems from which safe information about the original system can be inferred. We study two abstraction techniques shape analysis, a technique from program analysis, and data type reduction, originating from model checking. Until recently we did not properly understand how shape analysis and data type reduction relate. In this talk, we shed light on this relation in a comprehensive way. This is a step towards a more unified view of abstraction employed in the static analysis and model checking community. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Björn Wachter 2006 Is Part Of OASIcs, Volume 3, Workshop on Trustworthy Software (2006) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.TrustworthySW.2006.701 urn:nbn:de:0030-drops-7016 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.701 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode