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


  • 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


Email: tie.cheng [at]
Address: Computer Science Department, École Normale Supérieure, 45 rue d'Ulm, 75005 Paris, France