Publications de Philippe Paul Henri Suter

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

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

Philippe Paul Henri Suter, Viktor Kuncak

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

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

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

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

2011

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Philippe Paul Henri Suter, Robin Steiger, Viktor Kuncak

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

Philippe Paul Henri Suter, Viktor Kuncak

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

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

Building a Calculus of Data Structures

Philippe Paul Henri Suter, Viktor Kuncak, Ruzica Piskac

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets ...

Springer2010

Comfusy: A Tool for Complete Functional Synthesis

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

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesi ...

Springer2010

Decision Procedures for Algebraic Data Types with Abstractions

Mirco Dotta, Philippe Paul Henri Suter, Viktor Kuncak

We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term a ...

2010

Ordered Sets in the Calculus of Data Structures

Philippe Paul Henri Suter, Viktor Kuncak, Ruzica Piskac

Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints with a rich set of operations. A key challenge is to define such classes of ...

Springer2010

Complete Functional Synthesis

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

2010