AiXL: a Spreadsheet Application Verifier

Summary

By providing abstractions for complex data-structures, the MemCAD project has openened the way to the static analysis and verification of Spreadsheet Applications. During my PhD thesis, I have 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 analyzer verifies spreadsheets by types. For instance, ill-typed operations such as comparisons of integer values with string values are deemed suspicious, and can be clues to spreadsheet defects. Thus, the analyzer either raises alarms if such operations may emerge in a future execution of a spreadsheet, or proves that the spreadsheet is exempt of a class of typing errors.

The industrialization of the analyzer is undertaken by MatrixLead, a startup created by myself.

People

• Tie Cheng, former PhD Student and post-doc at ENS Paris, now CEO of MatrixLead
  
• Xavier Rival, Research Director at INRIA Paris-Rocquencourt and head of the ANTIQUE Project-Team, Scientific Adviser of MatrixLead

Publications

• Static Analysis of Spreadsheet Applications, PhD thesis, 2015, Tie Cheng
  [abstract]
• Static Analysis of Spreadsheet Applications for Type-Unsafe Operations Detection, In the 24th European Symposium on Programming (ESOP 2015), Tie Cheng, Xavier Rival
  [abstract | pdf]
• An Abstract Domain to Infer Types over Zones in Spreadsheets, In the 19th International Static Analysis Symposium (SAS 2012), Tie Cheng, Xavier Rival
  [abstract | pdf]