Viktor Kuncak
Il - He/him
EPFL IC IINFCOM LARA
INR 318 (Bâtiment INR)
Station 14
1015 Lausanne
+41 21 693 52 81
+41 21 693 49 43
Office:
INR 318
EPFL › IC › IINFCOM › LARA
Website: https://lara.epfl.ch
+41 21 693 52 81
Office:
INR 318
EPFL › IC › IC-SIN › SIN-ENS
Website: https://sin.epfl.ch
+41 21 693 52 81
Office:
INR 318
EPFL › IC › IC-SSC › SSC-ENS
Website: https://ssc.epfl.ch
Expertise
Mission
Detailed page
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
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)