Viktor Kuncak

Il - He/him

EPFL IC IINFCOM LARA
INR 318 (Bâtiment INR)
Station 14
1015 Lausanne

Expertise

automated reasoning, formal verification

Mission

Helping construct software that does what we expect

Detailed page

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 15 completed PhD theses. He works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article.  The answer to the big question of his citations, according to Google Scholar, is around 45. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he taught courses on functional and parallel programming, compilers, and verification; at Coursera he co-taught the MOOC "Parallel Programming".

Awards

ERC grant

European Research Council

2012

Selected publications

Deciding Boolean Algebra with Presburger Arithmetic

Viktor Kuncak, Hai Huu Nguyen, and Martin Rinard
Published in Journal of Automated Reasoning, 36(3), 2006 in

Modular Pluggable Analyses for Data Structure Consistency

Viktor Kuncak, Patrick Lam, Karen Zee, and Martin Rinard
Published in IEEE Transactions on Software Engineering, 32(12), 2006 in

Relational Analysis of Algebraic Datatypes

Viktor Kuncak and Daniel Jackson
Published in Joint 10th European Software Engineering Conference and 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2005 in

Structural Subtyping of Non-Recursive Types is Decidable

Viktor Kuncak and Martin Rinard
Published in Eighteenth Annual IEEE Symposium on Logic in Computer Science, 2003 in

Role Analysis

Viktor Kuncak and Patrick Lam and Martin Rinard
Published in Proceedings of the 29th Annual ACM Symposium on Principles of Programming Languages, 2002 in

Infoscience

Teaching & PhD

PhD Students

Matthieu Bovel, Auguste Poiroux, Sankalp Gambhir, Samuel Chassot, Lazar Milikic

Past EPFL PhD Students

Ruzica Piskac, Philippe Suter, Hossein Hojjat, Eva Darulova, Tihomir Gvero, Etienne Kneuss, Régis William Blanc, Mikaël Mayer, Qiang Wang, Ravichandhran Kandhadai Madhavan, Nicolas Voirol, Manos Koukoutos, Romain Edelmann, Georg Stefan Schmid, Rodrigo Raya, Dragana Milovancevic, Simon Guilloud

Past EPFL PhD Students as codirector

Giuliano Losa, Milos Nikolic

Courses

Computer language processing

CS-320

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into machine code using a popular backend called LLVM (https://llvm.org)

Formal Mathematics with Lean and AI

CS-643

This graduate course provides an introduction to using Lean proof assistant to formalize mathematical definitions and theorems. We will have lectures on foundations (formal proofs, dependent type theory), learn about practice (proof tactics, use of AI, etc) and work on a formalization project.

Formal verification

CS-550

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

Software construction

CS-214

Learn how to design and implement reliable, maintainable, and efficient software using a mix of programming skills (declarative style, higher-order functions, inductive types, parallelism) and fundamental software construction concepts (reusability, abstraction, encapsulation, composition, proofs)