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–12EPFL, PhD. Computer Science
2006–08EPFL, MSc. Computer Science
2008MIT, Visiting student
2003–06EPFL, BSc. Computer Science
2006ETH Zürich, Research intern
2005–06McGill University, Exchange year

Contact

+1 (914) 945-1611
IBM T.J. Watson Research Center
1101 Kitchawan Road
Yorktown Heights, NY 10598
| | | |

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

Teaching

I TA'd the following courses:

  • Compiler Construction, in 2008, 2009, 2010, and 2011.
  • Theoretical Computer Science, in 2010.
  • Software Analysis and Verification, in 2009.