Viktor Kuncak

Viktor Kuncak is an Associate Professor and head of the Laboratory for Automated Reasoning and Analysis (LARA) at EPFL. He joined EPFL in 2007 after completing his PhD at MIT. His research focuses on formal verification, automated reasoning, programming languages, and program synthesis. He has led significant initiatives such as the European COST Action on automated reasoning formats and secured a 5-year ERC grant (2012–2017).

Education: PhD in Computer Science from MIT (2007), MSc in Computer Science and Physics from MIT (2001), BSc in Computer Science from University of Novi Sad (2000).

Research Interests: Formal methods, automated theorem proving, program analysis, and tools for software verification. His work bridges theoretical foundations and practical systems, with contributions to verifiers like Leon and Stainless.

Recent work emphasizes verified compilers, set theory formalisms, and education tools like Lisa. His publications address challenges in SMT solving, equivalence checking, and functional programming.

• Scientific Awards: ERC Starting Grant (2012), ACM SIGSOFT Distinguished Paper (2010), CAV Best Paper (2010).

Advising: Supervised 16 completed PhD theses, with current students working on proof assistants and formal verification frameworks. Grants include SNSF and EU-funded projects.

Labs/Teams: Directs LARA lab at EPFL, collaborating with global researchers in formal methods and programming languages.