MemCAD ERC Project

Xavier Rival


The MemCAD project aims at designing a framework for the static analysis of programs manipulating complex memory states. A very wide range of data structures are encountered in real programs, such as arrays, linked structures, strings... While static analysis techniques have been developped to deal with each of those issues, no framework allows to deal with all of them in a single analysis tool. The purpose of the MemCAD project is to propose ways to combine analysis techniques adapted to simpler data structures so as to infer precise invariants about programs manipulating complex data structures, composed of intricate combinations of basic ones.

MemCAD Analyzer: a Memory Abstraction Platform

In the course of the MemCAD project, the MemCAD analyzer is being developped at INRIA, in the ANTIQUE (ANalyse staTIQUE) Project Team. The MemCAD analyzer is a research tool, meant to serve as a basis for the implementation and the evaluation of abstractions for complex data-structures. We have implemented a number of memory abstractions including:

The current version of the MemCAD Analyzer is available in Opam. See here for the package description.

AiXL: a Spreadsheet Application Verifier

By providing abstractions for complex data-structures, the MemCAD project has openened the way to the static analysis and verification of Spreadsheet Applications. During his PhD Thesis, Tie Cheng has implemented AiXL, a static analyzer for Spreadsheet Applications, that supports:

The industrialization of tools for the verification of Spreadsheet Applications is the focus of MatrixLead, a startup created by Tie Cheng (Tie Cheng serves as CEO of MatrixLead, and Xavier Rival as Scientific Adviser).


Current members:

Former members: