My current research interests include automated reasoning on high-level specifications to recursive functional programs. I am also interested in static analysis techniques for functional and object oriented programs written in Scala. I have for instance investigated techniques to precisely and efficiently analyze memory side-effects in the presence of callbacks.
I have also looked at static reasoning techniques for highly-dynamic languages such as PHP.
Leon is an automated system for
Insane is a combination of a pointer analysis with a memory effect analysis for the Scala programming language. Our analysis is based on abstract interpretation, it is inter-procedural and flow sensitive. The analysis, aimed at higher order programs, computes compositional summaries using a very expressive representation of effects and does not require annotations. This analysis is implemented as an extension of the reference compiler.
Phantm analyzes PHP code statically (with optional help from dynamic instrumention). It reconstructs types of variables at all program points using abstract interpretation. While estimating types, it also checks whether the operations on the corresponding values are well-defined.
Counterexample-Complete Verification for Higher-Order Functions
Scala Symposium 2015,
Deductive Program Repair
Synthesis Modulo Recursive Functions
Effect Analysis for Programs with Callbacks
An Overview of the Leon Verification System
Phantm: PHP Analyzer for Type Mismatch (Research Demonstration)
Runtime Instrumentation for Precise Flow-Sensitive Type Analysis
Toward Interprocedural Pointer and Effect Analysis for Scala
Master Thesis, 2011,