MAGIC-LogoMAGIC : Modular Analysis of proGrams In C


October 28, 2004NEW The ComFoRT reasoning framework is being developed on top of MAGIC.
June 5, 2004  MAGIC version 1.0  available for download.
July 29, 2003 MAGIC version 0.1  available for download.

Project Files

Version
Source
Binaries
Manual
Tutorial
1.0
magic-1.0.tar.gz
RH-7.1 RH-8.0 RH-9.0 Win32 manual-1.0
tutorial-1.0
0.1 magic-0.1.tar.gz RH-7.1 RH-8.0 RH-9.0 Win32
manual-0.1 tutorial-0.1

Please see the respective manuals for installation instructions. Also look at the ChangeLog for important differences between various releases.

Table of Contents

Introduction

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. First, a finite model is extracted from the component implementation using various abstraction tecnhiques, e.g. predicate abstraction. Next the model is verified against the specification. If a counterexample is found, its validity is checked and the model is refined successively to get rid of spurious counterexamples.

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. We are attempting to develop better technques for mitigating the statespace explosion that arises out of the interleaving of multiple processes or threads of control and of the complexity that arises out of shared memory based communication. We are also trying to validate the effectiveness of MAGIC in verifying real-life industrial applications.

Back to Top

ChangeLog

Difference between Version 1.0 and Version 0.1
Version 0.1 : Base release.

Back to Top

Publications

Journal

Conference

Workshop

Technical Report

Back to Top

People

MAGIC is being undertaken by members of the Model Checking Group at CMU. Various researchers have critically contributed, and continue to contribute, to its development. Below is a non-exhaustive list of some of them.
We also have ongoing collaborations with members of the PACC project at the Software Engineering Institute aimed at analysing component-based systems.

Back to Top

Related Projects

Primarily Software
Verification

Primarily Hardware
Verification

Theorem
Provers
SAT
Solvers

Back to Top

Contact Info

We will be delighted to get feedback from you. If you have questions and/or comments or if you want to be notified about changes and updates to the MAGIC website or its official release, please email me. This page is constantly under construction and will be updated on a regular basis. So please drop by again soon.

Back to Top


HOME