Memory Compositional Abstract Domains
MemCAD ERC Starting Grant (Oct. 2011 -
Oct 2016)
Summary
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
In the course of the MemCAD project, the MemCAD analyzer is being
developped at INRIA.
We plan to release source code of the analyzer along the course of the
project.
People
Current members:
- Xavier Rival, CR1 INRIA Paris Rocquencourt,
Abstraction Project Team, PI
- Bor-Yuh Evan Chang,
Assistant Professor at the University of Colorado at Boulder
at ENS Paris
- Arnaud Spiwack,
Post-Doc at Inria/ENS Paris, since September 2012.
- Tie Cheng,
PhD Student at ENS Paris, since October 2011
- Antoine Toubhans,
PhD Student at ENS Paris, since October 2011
Former member:
- Pascal Sotin, Post Doc
at ENS Paris (2011-2012), now Assistant Professor (Maìtre de
Conférences) at IRIT and IUT Blagnac
Publications
- Antoine Toubhans, Bor-Yuh Evan Chang and Xavier Rival.
Reduced Product Combination of Abstract Domains for Shapes.
In Verification, Model Checking and Abstract Interpretation 2013
(VMCAI'13).
[.pdf]
- Hierarchical Abstraction of Dynamic Structures.
Pascal Sotin and Xavier Rival.
In Asian Conference on Programming Languages And Software 2012.
[.pdf]
- An Abstract Domain to Infer Types over Zones in Spreadsheets.
Tie Cheng and Xavier Rival.
In Static Analysis Symposium (SAS'12).
[.pdf]