Publications by Etienne Kneuss

An Update on Deductive Synthesis and Repair in the Leon Tool

Etienne Kneuss, Viktor Kuncak, Emmanouil Koukoutos

We report our progress in scaling deductive synthesis and repair of recursive functional Scala programs in the Leon tool. We describe new techniques, including a more precise mechanism for encoding the space of meaningful candidate programs. Our techniques ...

2017

Deductive Synthesis and Repair

Etienne Kneuss

In this thesis, we explore techniques for the development of recursive functional programs over unbounded domains that are proved correct according to their high-level specifications. We present algorithms for automatically synthesizing executable code, st ...

EPFL2016

Deductive Program Repair, Computer Aided Verification

Etienne Kneuss, Viktor Kuncak

We present an approach to program repair and its application to programs with recursive functions over unbounded data types. Our approach formulates program repair in the framework of deductive synthesis that uses existing program structure as a hint to gu ...

2015

Synthesizing Functions from Relations in Leon

Etienne Kneuss, Viktor Kuncak, Emmanouil Koukoutos

Springer-Verlag Berlin2015

Synthesis Modulo Recursive Functions

Philippe Paul Henri Suter, Etienne Kneuss, Viktor Kuncak, Ivan Kuraj

We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synt ...

2013

An overview of the Leon verification system: verification by translation to recursive functions

Philippe Paul Henri Suter, Régis William Blanc, Etienne Kneuss, Viktor Kuncak

We present the Leon verification system for a subset of the Scala programming language. Along with several functional features of Scala, Leon supports imperative constructs such as mutations and loops, using a translation into recursive functional form. Bo ...

2013

Effect Analysis for Programs with Callbacks

Philippe Paul Henri Suter, Etienne Kneuss, Viktor Kuncak

We introduce a precise interprocedural effect analysis for programs with mutable state, dynamic object allocation, and dynamic dispatch. Our analysis is precise even in the presence of dynamic dispatch where the context-insensitive estimate on the number o ...

Springer Berlin Heidelberg2013

Phantm: PHP analyzer for type mismatch

Philippe Paul Henri Suter, Etienne Kneuss, Viktor Kuncak

We present Phantm, a static analyzer that uses a flow-sensitive analysis to detect type errors in PHP applications. Phantm can infer types for nested arrays, and can leverage runtime information and procedure summaries for more precise results. Phantm foun ...

2010