Bounded Model Checking (BMC) offers the possibility to proof the correctness of an implementation of a digital hardware system. To enhance the capabilities, abstraction techniques were developed. This contribution introduces an experimental software called tudapc applying automatic abstraction techniques to BMC.

Contact:
Ingo Schäfer (schaefer@rs.tu-darmstadt.de)