MAGIC : Modular Analysis of proGrams In C

October 28, 2004	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

Table of Contents

• Introduction
• ChangeLog
  
• Publications
• People
• Related Projects
• Contact Info

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

• Return actions now written as return {$0 == 10} instead of return {10}. In general a return action is of the form return {expression} where expression can capture arbitrary conditions on the return value. The return value itself is represented by the dummy variable $0. For instance the action return {$0 < 5} expresses the return of a value less than 5.
  

• New options: Please look at the command-line options section in the manual.
  

Version 0.1 : Base release.

Back to Top

Publications

Journal

• Modular Verification of Software Components in C, Transactions on Software Engineering (TSE), Volume 30, Number 6, pages 388-402, June 2004, Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith. © IEEE, 2004. This is the author's version of the work. It is posted here by permission of IEEE for your personal use. Not for redistribution ( ps ps.gz pdf ).

• Efficient Verification of Sequential and Concurrent C Programs, Formal Methods in System Design (FMSD),Volume 25, Issue 2-3, pages 129-166, September-November 2004, Sagar Chaki, Edmund Clarke, Alex Groce, Joel Ouaknine, Ofer Strichman, Karen Yorav. © Springer, 2004. This is the author's version of the work. It is posted here by permission of Springer for your personal use. Not for redistribution ( ps ps.gz pdf ).

Conference

• Explaining Abstract Counterexamples, 12th International Symposium on Foundations of Software Engineering (FSE) 2004, Sagar Chaki, Alex Groce, Ofer Strichman, ( ps ps.gz pdf ). This paper describes a technique for explaining the cause behind counterexamples obtained by model checking predicate abstractions of C programs.
  

• Automated, compositional and iterative deadlock detection, Second ACM-IEEE International Conference on Formal Methods and models for Codesign (MEMOCODE) 2004, Sagar Chaki, Edmund Clarke, Joel Ouaknine, Natasha Sharygina, ( ps ps.gz pdf ). This paper describes a compositional technique based on counterexample guided abstraction refinement to detect deadlocks in concurrent systems.
  

• State/Event-based Software Model Checking, Fourth International Conference on Integrated Formal Methods (IFM) 2004, LNCS 2999, pages 128-147, Sagar Chaki, Edmund Clarke, Joel Ouaknine, Natasha Sharygina, Nishant Sinha, ( ps ps.gz pdf ). This is a revised and extended version of our workshop publication with the same title described below.

• Predicate Abstraction with Minimum Predicates, 12th Advanced Research Working Conference  on Correct Hardware Design and Verification Methods (CHARME) 2003, LNCS 2860, pages 19-34, Sagar Chaki, Edmund Clarke, Alex Groce, Ofer Strichman, ( ps ps.gz pdf ). This paper describes a technique for obtaining a minimum number of predicates during predicate abstraction and CEGAR driven verification of C programs. The technique is based on solving pseudo-Boolean constraints.

• Modular Verification of Software Components in C, An ACM-SIGSOFT Distinguished Paper in the 25th International Conference on Software Engineering (ICSE) 2003, pages 385-395, Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, Helmut Veith, ( ps ps.gz pdf ). This is the basic paper introducing MAGIC and explaining the technical details behind the extraction of finite models from software components written in C. Revised and extended version appeared as invited article in a special issue of Transactions on Software Engineering (TSE) (see above).

Workshop

• State/Event-based Software Model Checking, Workshop on State-oriented vs. Event-oriented thinking in Requirements Analysis, Formal Specification and Software Engineering (ST.EVE) 2003, Sagar Chaki, Joel Ouaknine, Natasha Sharygina, Nishant Sinha, ( ps ps.gz pdf ). This paper presents an LTL-like logic and associated formalism for expressing properties that deal with both states and events of a state-event based system. It also presents preliminary experimental evidence suggesting that such an approach could be practically advantageous.
  

• Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach, 2nd Workshop on Software Model Checking (SoftMC) 2003, ENTCS 89(3), Boulder, Colorado, July 2003, Sagar Chaki, Joel Ouaknine, Karen Yorav, Edmund Clarke, ( ps ps.gz pdf ). This paper describes a two-level abstraction refinement framework for efficiently verifying concurrent C programs.

Technical Report

• An Expressive Verification Framework for State/Event Systems, Technical report # CMU-CS-04-145, Computer Science Department, School of Computer Science, Carnegie Mellon University, Sagar Chaki, Edmund Clarke, Orna Grumberg, Joel Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith, ( ps pdf ).
  

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.

• Sagar Chaki
• Edmund Clarke
• Alex Groce
• Somesh Jha
• Joel Ouaknine
• Natasha Sharygina
• Nishant Sinha
  
• Ofer Strichman
• Tayssir Touili
  
• Helmut Veith
• Karen Yorav

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
SPIN Verisoft Bandera Java PathFinder Bogor	SLAM BLAST CBMC CMC	CMU-SMV Cadence-SMV Verus MOCHA MUR-Ø NuSMV UCLID	Simplify SVC CVC ICS CProver CVC-Lite	Grasp Chaff PBS

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