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: 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:

• abstractions for recursive dynamic structures based on separation logic and inductive definitions;
• abstractions for array structures, based on non contiguous partitions;
• separating product, reduced product and hierarchical product functors;
• product with numeric and set abstractions;
• silhouettes for the guiding of unions of abstract states.

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:

• spreadsheet table contents abstraction based on zones;
• spreadsheet formulas;
• macros modifying the table dynamically.

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).

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.
• Hugo Illous, PhD Student at CEA and ENS Paris, co-supervised with Matthieu Lemerre.
• Huisong Li, PhD Student at ENS Paris.
• Jiangchao Liu, PhD Student at ENS Paris.
• Changhee Park, Post-doctorate researcher.

Former members:

• François Béranger, Research Engineer.
• Tie Cheng, former PhD Student at ENS Paris (graduated in September 2015).
• Guillaume Cluzel summer intern.
• Arlen Cox, former PhD Student at University of Colorado at Boulder and ENS Paris, co-advised with Bor-Yuh Evan Chang (graduated in November 2014).
• Pascal Sotin, Post Doc at ENS Paris (2011-2012), now Assistant Professor (Maìtre de Conférences) at IRIT and IUT Blagnac.
• Arnaud Spiwack, Post-Doc at Inria/ENS Paris, from September 2012 to August 2014.
• Antoine Toubhans, PhD Student at ENS Paris, from October 2011 until December 2015.
• Pippijn Van Steenhoeven, Research Engineer, now Engineer at Google.
• Yoonseok Ko, PhD Intern, Currently Graduate student at KAIST

Publications

• A Relational Shape Abstract Domain. Hugo Illous, Matthieu Lemerre and Xavier Rival. In Nasa Formal Methods Symposium (NFM'17).
• Semantic-Directed Clumping of Disjunctive Abstract States, ACM Symposium on Principles of Programming Languages (POPL 2017), 2017 Huisong Li, Francois Berenger, Bor-Yuh Evan Chang and Xavier Rival. In Principles Of Programming Languages 2017 (POPL'17), Paris, Jan. 2017. (VM).
• An array content static analysis based on non-contiguous partitions. Jiangchao Liu and Xavier Rival. In Computers, Languages, Systems and Structures, January 2016, Elsevier. [.pdf]
• Abstraction of Optional Numerical Values. Jiangchao Liu and Xavier Rival. In Asian Conference on Programming Languages And Software (APLAS'15), Pohang (South Korea), December 2015, Lecture Notes in Computer Science 9458, pages 146--166, Springer. [.pdf]
• Abstract Domains and Solvers for Sets Reasoning. Arlen Cox, Bor-Yuh Evan Chang, Huisong Li and Xavier Rival. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15), Suva (Fidji), December 2015, Lecture Notes in Computer Science 9450, pages 356--371, Springer. [.pdf]
• Shape Analysis for Unstructured Sharing. Huisong Li, Xavier Rival, Bor-Yuh Evan Chang. In Static Analysis Symposium (SAS'15), Saint-Malo (France), September 2015, Lecture Notes in Computer Science 9291, pages 90--108, Springer. [.pdf]
• Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages. Arlen Cox, Bor-Yuh Evan Chang and Xavier Rival. In European Symposium On Programming (ESOP'15), London (UK), April 2015. [.pdf] (to appear).
• Static Analysis of Spreadsheet Applications for the Detection of Type Unsafe Operations. Tie Cheng and Xavier Rival, In European Symposium On Programming (ESOP'15), London (UK), April 2015. [.pdf] (to appear).
• Abstraction of Arrays Based on Non-Contiguous Partitions. Jiangchao Liu and Xavier Rival, In Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'15), Mumbai (India), January 2015, Lecture Notes in Computer Science 8931, pages 375--395, Springer. [.pdf].
• Construction of Abstract Domains for Heterogeneous Properties. Antoine Toubhans, Bor-Yuh Evan Chang and Xavier Rival, In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'14), Corfu (Greece), October 2014, Lecture Notes in Computer Science 8803, pages 489--492, Springer. [.pdf].
• Automatic Analysis of Open Objects in Dynamic Language Programs. Arlen Cox, Bor-Yuh Evan Chang and Xavier Rival, In Static Analysis Symposium (SAS'14), Muenchen (Germany), September 2014, Lecture Notes in Computer Science 8723, pages 285--301, Springer. [.pdf].
• An Abstract Domain Combinator for Separately Conjoining Memory Abstractions. Antoine Toubhans, Bor-Yuh Evan Chang and Xavier Rival, In Static Analysis Symposium (SAS'14), Muenchen (Germany), September 2014, Lecture Notes in Computer Science 8723, pages 285--301, Springer. [.pdf].
• Modular Construction of Shape-Numeric Analyzers. Bor-Yuh Evan Chang and Xavier Rival, In Festschrift for Dave Schmidt, Manhattan (Kansas, USA), September 2013, Electronic Proceedings in Theoretical Computer Science 129, pages 161--185, EPTCS. [.pdf].
• Reduced Product Combination of Abstract Domains for Shapes. Antoine Toubhans, Bor-Yuh Evan Chang and Xavier Rival. 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 (APLAS'2012). [.pdf]
• An Abstract Domain to Infer Types over Zones in Spreadsheets. Tie Cheng and Xavier Rival. In Static Analysis Symposium (SAS'12). [.pdf]
• Abstract Domains for the Analysis of Programs Manipulating Complex Data-Structures. Xavier Rival. Habilitation Thesis. [.pdf]