Viktor Kuncak

Registered user since Thu 9 Jul 2015

Name: Viktor Kuncak

Bio: Viktor Kuncak is an associate professor in the EPFL School of Computer and Communication Sciences, where he leads the Laboratory for Automated Reasoning and Analysis ( He works in formal methods with emphasis on algorithms and tools, such as Leon ( He received a PhD degree from the Massachusetts Institute of Technology (MIT) in 2007. He was a program co-chair of FMCAD 2014 and VMCAI 2012, and led an international COST Action to establish standardized formats for verification and synthesis (Rich Model Toolkit). His invited talks include those at LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. He received an ACM SIGSOFT distinguished paper award for work on automated testing. His work on software synthesis procedures was published in the Communications of the ACM as a Research Highlight article. His recent work on Implicit Programming, funded by a European Research Council (ERC) grant, aims to bridge the gap between human goals and their computational realizations.

Affiliation: EPFL, Switzerland

Personal website:

Research interests: program synthesis, verification, and analysis; automated reasoning


PEPM 2019Committee Member in Program Committee within the PEPM 2019-track
SPLASH 2019Committee Member in External Review Committee within the OOPSLA-track
Author of Type-Theoretic Foundation of an SMT-Based Verifier within the OOPSLA-track
VMCAI 2019Author of Minimal Synthesis of String To String Functions From Examples within the VMCAI 2019-track
SPLASH 2018Author of Bidirectional Evaluation with Direct Manipulation - Artifact Evaluation within the Artifacts-track
Author of Bidirectional Evaluation with Direct Manipulation within the OOPSLA-track
Scala 2016Author of SMT-Based Checking of Predicate-Qualified Types for Scala within the Scala-track
POPL 2017Author of Contract-based Resource Verification for Higher-order Functions with Memoization within the POPL-track
ECOOP 2017Author of Proactive Synthesis of Recursive Tree-to-String Functions from Examples within the ECOOP Research Papers-track
POPL 2016Committee Member in Program Committee within the Research Papers-track
Committee Member in Program Committee
SPLASH 2015Author of Synthesizing Java Expressions from Free-Form Queries within the OOPSLA-track
Author of Programming with Enumerable Sets of Structures within the OOPSLA-track
Author of Automating Grammar Comparison within the OOPSLA-track
Author of Automating Grammar Comparison within the OOPSLA Artifacts-track
Onward! 2013Author of Game Programming by Demonstration within the Research Papers-track
Author of Synthesis Modulo Recursive Functions within the OOPSLA-track
SPLASH 2012Committee Member in External Reviewers within the OOPSLA Research Papers-track