**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

Person# Philippe Paul Henri Suter

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related units

Loading

Courses taught by this person

Loading

Related research domains

Loading

Related publications

Loading

People doing similar research

Loading

Courses taught by this person

No results

Related units (1)

Related publications (35)

Loading

Loading

Loading

Related research domains (20)

Algorithm

In mathematics and computer science, an algorithm (ˈælɡərɪðəm) is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algo

Boolean satisfiability problem

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining i

Boolean algebra

In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values true and false,

People doing similar research (117)

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

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way—they should succeed for a well-defined class of specifications. To guarantee correctness and applicability to software (and not just hardware), these algorithms should also support unbounded data types, such as numbers and data structures. To obtain appropriate synthesis algorithms, we propose to generalize decision procedures into predictable and complete synthesis procedures. Such procedures are guaranteed to find the code that satisfies the specification if such code exists. Moreover, we identify conditions under which synthesis will statically decide whether the solution is guaranteed to exist and whether it is unique. We demonstrate our approach by starting from a quantifier elimination decision procedure for Boolean algebra of set with Presburger arithmetic and transforming it into a synthesis procedure. Our procedure also works in the presence of parametric coefficients. We establish results on the size and the efficiency of the synthesized code. We show that such procedures are useful as a language extension with implicit value definitions, and we show how to extend a compiler to support such definitions. Our constructs provide the benefits of synthesis to programmers, without requiring them to learn new concepts, give up a deterministic execution model, or provide code skeletons.

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

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. Both properties and programs in Leon are expressed in terms of user-defined functions. We discuss several techniques that led to an efficient semi-decision procedure for first-order constraints with recursive functions, which is the core solving engine of Leon. We describe a generational unrolling strategy for recursive templates that yields smaller satisfiable formulas and ensures completeness for counterexamples. We illustrate the current capabilities of Leon on a set of examples, such as data structure implementations; we show that Leon successfully finds bugs or proves completeness of pattern matching as well as validity of function postconditions.

2013, ,

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 of targets is very large. This feature makes our analysis appropriate for programs that manipulate first-class functions (callbacks). We present a framework in which programs are enriched with special effect statements, and define the semantics of both program and effect statements as relations on states. Our framework defines a program composition operator that is sound with respect to relation composition. Computing the summary of a procedure then consists of composing all its program statements to produce a single effect statement. We propose a strategy for applying the composition operator in a way that balances precision and efficiency. We instantiate this framework with a domain for tracking read and write effects, where relations on program states are abstracted as graphs. We implemented the analysis as a plugin for the Scala compiler. We analyzed the Scala standard library containing 58000 methods and classified them into several categories according to their effects. Our analysis proves that over one half of all methods are pure, identifies a number of conditionally pure methods, and computes summary graphs and regular expressions describing the side effects of non-pure methods.