Skip to Content

Bounded Model Checker Using Property Based Automated Abstractions

0
Your rating: None
(unregistered) Author(s): 
Ingo Schäfer

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)