Etienne Kneuss


BC 355 (BC Building)
Station 14
CH-1015 Lausanne


2011-2016EPFL, PhD. Computer Science
2009-2011EPFL, MSc. Computer Science
2006-2009EPFL, BSc. Computer Science

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

More information

Try it online!


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.

More information


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.

More information


In Proceedings

Counterexample-Complete Verification for Higher-Order Functions
N. Voirol, E. Kneuss and V. Kuncak, Scala Symposium 2015
Deductive Program Repair
E. Kneuss, M. Koukoutos and V. Kuncak, CAV 2015
Synthesis Modulo Recursive Functions
E. Kneuss, V. Kuncak, I. Kuraj and P. Suter, OOPSLA 2013
Effect Analysis for Programs with Callbacks
E. Kneuss, V. Kuncak and P. Suter, VSTTE 2013
An Overview of the Leon Verification System
R. W. Blanc, E. Kneuss, V. Kuncak and P. Suter, SCALA 2013
Phantm: PHP Analyzer for Type Mismatch (Research Demonstration)
E. Kneuss, P. Suter and V. Kuncak, FSE 2010
Runtime Instrumentation for Precise Flow-Sensitive Type Analysis
E. Kneuss, P. Suter and V. Kuncak, RV 2010


Toward Interprocedural Pointer and Effect Analysis for Scala
E. Kneuss, Master Thesis, 2011