Welcome to the homepage of the MAGIC project. The aim of this project is to develop tools and techniques for analyzing and reasoning about software components written in the C programming language. The overall goal of MAGIC is to check conformance between component specifications and their implementations. The implementations could be concurrent i.e. composed of multiple threads or processes communicating via messages or shared memory. To this end, MAGIC follows the counterexample guided abstraction refinement paradigm.

Further, the MAGIC framework is compositional. Using MAGIC, the problem of verifying a large implementation can be naturally decomposed into the verification of a number of smaller, more manageable fragments. These fragments can be verified separately, enabling MAGIC to scale up to industrial size programs. Currently, the focus of our research is on improved handling of concurrency and shared memory.