Software

Ddisasm

Ddisasm is a disassembler written in Datalog. It produces reassembleable assembly and it uses the Souffle Datalog engine to achieve great speed.

Related publications:

• Datalog Disassembly

CoFloCo (github)

I developed CoFloCo, a static analysis tool to infer automatically symbolic complexity upper and lower bounds of imperative and recursive programs. CoFloCo’s analysis is not binded to any specific programming language, instead it takes an abstract representation of programs as an input. The abstract representation is a set of cost equations that can be generated from source code, bytecode or other intermediate representations.

Related publications:

• Cost Analysis of Programs Based on the Refinement of Cost Relations
• Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
• Resource Analysis of Complex Programs with Cost Equations

SACO

I participated in the development of SACO, a static analyzer for concurrent objects. It analyzes programs written in ABS and performs the following static analyses:

• Termination and Resource analysis
• Deadlock analysis

In addition, SACO performs auxiliary static analyses:

• Points-to analysis
• May-happen-in-parallel:

  • May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization

  • May-Happen-in-Parallel Analysis for Actor-based Concurrency