Publications de Philippe Paul Henri Suter

Synthesis Modulo Recursive Functions

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter, 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

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

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

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter

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

Programming with Specifications

Philippe Paul Henri Suter

This thesis explores the use of specifications for the construction of correct programs. We go beyond their standard use as run-time assertions, and present algorithms, techniques and implementations for the tasks of 1) program verification, 2) declarative ...

EPFL2012

Constraints as Control

Viktor Kuncak, Philippe Paul Henri Suter

We present an extension of Scala that supports constraint programming over bounded and unbounded domains. The resulting language, Kaplan, provides the benefits of constraint programming while preserving the existing features of Scala. Kaplan integrates con ...

2012

Software Synthesis Procedures

Viktor Kuncak, Mikaël Mayer, Philippe Paul Henri Suter, Ruzica Piskac

Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succ ...

2012

Scala to the Power of Z3: Integrating SMT and Programming

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

2011

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Viktor Kuncak, Philippe Paul Henri Suter, Robin Steiger

Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier- ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Scala to the Power of Z3: Integrating SMT and Programming

Viktor Kuncak, Philippe Paul Henri Suter

We describe a system that integrates the SMT solver Z3 with the Scala programming language. The system supports the use of the SMT solver for checking satisfiability, unsatisfiability, as well as solution enumeration. The embedding of formula trees into Sc ...

Springer-Verlag Berlin2011

Phantm: PHP analyzer for type mismatch

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter

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