Philippe Suter
I used to work in the Laboratory for Automated Reasoning and Analysis, where I obtained my PhD in December 2012 under the supervision of Viktor Kuncak. My dissertation focused on techniques for automated software verification and synthesis. As of June 2013, I work as a Research Staff Member at IBM.
Education
| 2008–12 | EPFL, PhD. Computer Science |
| 2006–08 | EPFL, MSc. Computer Science |
| 2008 | MIT, Visiting student |
| 2003–06 | EPFL, BSc. Computer Science |
| 2006 | ETH Zürich, Research intern |
| 2005–06 | McGill University, Exchange year |
Publications
| In proceedings | |
|---|---|
|
Synthesis Modulo Recursive Functions Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter, OOPSLA 2013, to appear |
|
|
Executing Specifications with Synthesis and Constraint Solving Viktor Kuncak, Etienne Kneuss, and Philippe Suter, RV 2013, to appear |
|
|
Effect Analysis for Programs with Callbacks Etienne Kneuss, Viktor Kuncak, and Philippe Suter, VSTTE 2013, to appear |
|
|
An Overview of the Leon Verification System Régis Blanc, Etienne Kneuss, Viktor Kuncak, and Philippe Suter, Scala 2013 |
|
|
Reductions for Synthesis Procedures Swen Jacobs, Viktor Kuncak, and Philippe Suter, VMCAI 2013 |
|
|
Constraints as Control Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter, POPL 2012 |
|
|
Satisfiability Modulo Recursive Programs Philippe Suter, Ali Sinan Köksal, and Viktor Kuncak, SAS 2011 |
|
|
Scala to the Power of Z3: Integrating SMT and Programming (System Description) Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter, CADE 2011 |
|
|
Sets with Cardinality Constraints in Satisfiability Modulo Theories Philippe Suter, Robin Steiger, and Viktor Kuncak, VMCAI 2011 |
|
|
Phantm: PHP Analyzer for Type Mismatch (Research Demonstration) Etienne Kneuss, Philippe Suter, and Viktor Kuncak, FSE 2010 |
|
|
Runtime Instrumentation for Precise Flow-Sensitive Type Analysis Etienne Kneuss, Philippe Suter, and Viktor Kuncak, RV 2010 |
|
|
Ordered Sets in the Calculus of Data Structures Viktor Kuncak, Ruzica Piskac, and Philippe Suter, CSL 2010 |
|
|
Comfusy: A Tool for Complete Functional Synthesis (Tool Presentation) Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter, CAV 2010 |
|
|
Complete Functional Synthesis Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter, PLDI 2010 |
|
|
Decision Procedures for Algebraic Data Types with Abstractions Philippe Suter, Mirco Dotta, and Viktor Kuncak, POPL 2010 |
|
|
Building a Calculus of Data Structures Viktor Kuncak, Ruzica Piskac, Philippe Suter, and Thomas Wies, VMCAI 2010 |
|
| Journal articles | |
|---|---|
|
Functional Synthesis for Linear Arithmetic and Sets Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter, to appear in STTT |
|
|
Software Synthesis Procedures Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter, CACM, February 2012 |
|
| Technical reports | |
|---|---|
|
On Static Analysis for Expressive Pattern Matching Mirco Dotta, Philippe Suter, and Viktor Kuncak, Technical report, Feb. 2008 |
|
| Miscellaneous | |
|---|---|
|
Les «Lieder ohne Worte» et l'esthétique romantique Aurélie Pala and Philippe Suter, Schweizer Musikzeitung/Revue Musicale Suisse, Feb. 2009 |
|
|
Non-Clausal Satisfiability Modulo Theories Philippe Suter, Master's Thesis, EPFL, Sep. 2008 |
|
Projects
Research
- Synthesis and implicit programming using formula-like specifications. See the Comfusy page, the Kaplan page, and the PLDI 2010 and POPL 2012 papers above.
- Verification of functional programs. See the LeonOnline demo, and our POPL 2010 and SAS 2011 papers above.
- Nenofar, a non-clausal SMT solver for the theory of uninterpreted function symbols. In collaboration with Vijay Ganesh.
Tools and More
- Scala Interface to Z3, JNI bindings and a Scala library to interact with the Z3 SMT solver.
- Cafebabe, a Scala library to generate Java bytecode.
- Bibimbap, a tool to import and manage BibTeX entries.
- BAPA/Z3, a theory plugin for Z3 to support sets with cardinality constraints.
- A list of upcoming conferences and deadlines in my areas of interest.
- My rejected submission to the first issue of TinyToCS.