Philippe Suter

Biography

---

I received my Master in Computer Science with a specialization in Foundations of Software from EPFL in September 2008. Since then and for the last 1354 days, I have been working towards obtaining a PhD under the supervision of Viktor Kuncak in the Laboratory for Automated Reasoning and Analysis. (CV )

Education

---

2006	-	2008	:	EPFL, Lausanne, MS. Computer Science
		2008	:	Massachusetts Institute of Technology, Cambridge, Visiting student
2003	-	2006	:	EPFL, Lausanne, BS. Computer Science
2005	-	2006	:	McGill University, Montreal, Exchange year

Publications

---

In Proceedings

• Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. Constraints as Control. POPL 2012, pp. 151-164.  
• Philippe Suter, Ali Sinan Köksal, and Viktor Kuncak. Satisfiability Modulo Recursive Programs. SAS 2011, pp. 298-315.
  
   
• Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. Scala to the Power of Z3: Integrating SMT and Programming (System Description). CADE 2011, pp. 400-406.
  
   
• Philippe Suter, Robin Steiger, and Viktor Kuncak. Sets with Cardinality Constraints in Satisfiability Modulo Theories. VMCAI 2011, pp. 403-418.
  
   
• Etienne Kneuss, Philippe Suter, and Viktor Kuncak. Phantm: PHP Analyzer for Type Mismatch (Research Demonstration). FSE 2010, pp. 373-374.  
• Etienne Kneuss, Philippe Suter, and Viktor Kuncak. Runtime Instrumentation for Precise Flow-Sensitive Type Analysis. RV 2010, pp. 300-314.
  
   
• Viktor Kuncak, Ruzica Piskac, and Philippe Suter. Ordered Sets in the Calculus of Data Structures. CSL 2010, pp. 34-48.
  
   
• Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. Comfusy: A Tool for Complete Functional Synthesis (Tool Presentation). CAV 2010, pp. 430-433.
  
   
• Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. Complete Functional Synthesis. PLDI 2010, pp. 316-329.  
• Philippe Suter, Mirco Dotta, and Viktor Kuncak. Decision Procedures for Algebraic Data Types with Abstractions. POPL 2010, pp. 199-210.  
• Viktor Kuncak, Ruzica Piskac, Philippe Suter, and Thomas Wies. Building a Calculus of Data Structures. VMCAI 2010, pp. 26-44.
  
   

Journal Articles

• Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. Functional Synthesis for Linear Arithmetic and Sets. To appear in STTT.
• Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. Software Synthesis Procedures. CACM, February 2012.

Technical Reports

• Mirco Dotta, Philippe Suter, and Viktor Kuncak. On Static Analysis for Expressive Pattern Matching. Technical report, Feb. 2008.

Miscellaneous

• Aurélie Pala and Philippe Suter. Les «Lieder ohne Worte» et l'esthétique romantique. Schweizer Musikzeitung/Revue Musicale Suisse, Feb. 2009, pp. 19-20.
• Philippe Suter. Non-Clausal Satisfiability Modulo Theories. 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.

Teaching

---

I TA'd or am TA'ing the following courses:

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