Jooyong Lee

BRICS, Department of Computer Science, Aarhus University, Denmark.

Time: Monday 14.3.2005, 13:00
Place: Room E3-109, Fr. Bajersvej 7E

Reverse Code Generation and Embedding for Program Model Checking

A model checker based on state space enumeration typically stores states for two purposes. One is to check if the state is visited before, and the other purpose is to backtrack to the previous state. If we accept small amount of coverage loss, the state-saving for the first purpose can be extremely economized by bitstate hashing, which squashes the state information into one bit. Then the memory used for backtracking becomes to occupy unfairly large amount of space. In this talk we will show a way to minimize the memory usage and with little time overhead for backtracking by introducing reverse code.