Tapir: Language Support to Reduce the State Space in Model-Checking

: 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 implemena 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.

• Type: Conference
• Year: 2009
• Where: GI
• Authors: Ronald Veldema, Michael Philippsen
• Keywords: GI 2009, Irrelevant Program Details, Specific Program Transformations, Tapir’s Aspect-oriented Test, Theoretical Computer Science