Model Checking Software via Abstraction of Loop Transitions

Natasha Sharygina, and James C. Browne

This paper reports a data abstraction algorithm that is targeted to minimize the contribution of the loop executions to the program state space. The loop abstraction is defined as the syntactic program transformation that results in the {\em sound} representation of the concrete program. The abstraction algorithm is defined and implemented in the context of the integrated software design, testing and model-checking. The loop abstraction technique was applied to verification of NASA robot control software. The abstraction enabled model checking for realistic robot configurations where all other approaches, including symbolic verification, predicate abstraction and partial order reduction failed.

Published in the Proceedings of the Fundamental Approaches to Software Engineering, 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, 15 pages.