Research

The focus of our research activities lies in the area of formal verification. This is motivated by the observervation that increasing system complexities and shorter development cycles make verification the bottleneck in the design process. Nowadays, verification consumes up to 80% of the development time.

We investigate techniques for formal and semiformal property checking. This includes model checking, temporal assertion checkers for simulators, bounded property checkers and related technologies.

The FMG strives to combine formal methods with real applications and tools, thus bridging the gap between theory and practice.

• RAVEN: A real-time model checker. Visit its website for detailed information.
  
• SymC: A BDD-based bounded property checker. Visit its website for more information.
• Temporal Checker for SystemC: Available at the download page of the European SystemC Users Group.