Gesellschaft fr Informatik e.V.

Lecture Notes in Informatics

INFORMATIK 2009 - Im Focus das Leben P-154, 2860-2874 (2008).

Gesellschaft für Informatik, Bonn


Stefan Fischer, Erik Maehle, Rüdiger Reischuk (eds.)

Copyright © Gesellschaft für Informatik, Bonn


Tapir: language support to reduce the state space in model-checking

Ronald Veldema and Michael Philippsen


Model-checking is a way of testing the correctness of concurrent programs. To do so, a model of the program is proven to match properties and constraints specified by the programmer. The model itself is created by disregarding irrelevant program details. The biggest problem in model-checking is the number of program states that need to be tested. Tapir, a simple but familiar object-oriented language and accompanying tool chain, addresses this problem in two ways. First, the programmer can provide application specific program transformations that reduce the state space. Second, for selected classes and methods, the programmer can provide an alternative implementation: a slim black box version for use in model-checking that abstracts away many details of the full fledged implementation. Tapir's aspect-oriented test case generation combined with black-boxing allows model-checking of low-level library code.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-3-88579-241-3

Last changed 24.01.2012 22:11:11