Viktor Kuncak

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

Web site:  Web site:  https://lara.epfl.ch

vCard
Administrative data

Fields of expertise

formal verification, theorem proving, program synthesis

Education

PhD

MIT

2007

Publications

Infoscience publications

Teaching & PhD

Teaching

Computer Science

Communication Systems

Courses

Software construction

Functional programming:
  • Functional programming paradigm
  • Recursion and tail-recursion
  • Evaluation strategies, lazy evaluation, substitution model
  • Modularity, data abstraction, representation independence
  • Subtyping, inheritance, type classes
  • Polymorphism, variance
  • Structural induction
  • Stateless parallelism, map-

Computer language processing

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 verification

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.