Complexity Analysis-based Guaranteed Execution

Charles Stark Draper Laboratory’s “Complexity Analysis-based Guaranteed Execution” (short title CAGE) builds on automated termination system and complexity analysis technology to formally guarantee the discovery of time and space vulnerabilities in software.

To develop CAGE, the Draper Team includes the leaders of the university research teams: Dr. Jurgen Giesl from the University of Aachen and Dr. Georg Moser from the University of Innsbruck, combined with Draper’s expertise in formal methods, static program analysis, and machine learning.

Duration: 4 years

Start of Project: May 1, 2015


Charles Stark Draper Laboratory project number

Draper Proposal Number: 15-B13



Running Interaction Nets on Random Access Machines
Stephane Gimenez and Georg Moser
Proceedings of the 8th International Workshop on Higher-Order Rewriting (HOR 2016),  2016.

Complexity of Acyclic Term Graph Rewriting
Martin Avanzini and Georg Moser
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Leibniz International Proceedings in Informatics 52, pp. 10:1 – 10:18, 2016.

Kruskal’s Tree Theorem for Term Graphs
Georg Moser and Maria A. Schett
Proceedings of the 9th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2016),  2016.

The Complexity of Interaction
Stéphane Gimenez and Georg Moser
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016),  243 – 255, 2016.