Viktor Kuncak

Expertise automated reasoning, formal verification Mission Helping construct software that does what we expect Detailed page https://lara.epfl.ch/~kuncak 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". 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) Awards ERC grant European Research Council 2012