View Abstraction – A Tutorial (Invited Paper)
Parosh Aziz Abdulla, Frédéric Haziza, Lukáš Holík · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2015
We consider parameterized verification, i.e., proving correctness of a system with an unbounded number of processes. We describe the method of view abstraction whose aim is to provide a small model property, i.e., showing correctness by only inspecting instances of the system consisting of a small fixed number of processes. We illustrate the method through an application to the classical Burns' mutual exclusion protocol.