Current Work
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.
Research Projects
Leon
Leon is an automated system for
- verifying functional Scala programs,
- finding counterexamples to the validity of user-specified properties,
- synthesizing programs from specifications and examples,
- repairing invalid programs.
Insane
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
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.
Publications
In Proceedings
|
Counterexample-Complete Verification for Higher-Order Functions
, Scala Symposium 2015
|
|
Deductive Program Repair
, CAV 2015
|
|
Synthesis Modulo Recursive Functions
, OOPSLA 2013
|
|
Effect Analysis for Programs with Callbacks
, VSTTE 2013
|
|
An Overview of the Leon Verification System
, SCALA 2013
|
|
Phantm: PHP Analyzer for Type Mismatch (Research Demonstration)
, FSE 2010
|
|
Runtime Instrumentation for Precise Flow-Sensitive Type Analysis
, RV 2010
|
Others
|
Toward Interprocedural Pointer and Effect Analysis for Scala
, Master Thesis, 2011
|