Prof. Viktor Kuncak

"Automating Construction of Provably Correct Software"

(Vortrag im Rahmen der "MPI Distinguished Lecture Series" in Kooperation mit dem Fachbereich Informatik)

I will present techniques my research group has been developing to transform reusable software specifications, suitable for users and designers, into executable implementations, suitable for efficient execution. I outline deductive synthesis techniques that transform input/output behavior descriptions (such as postconditions, invariants, and examples) into conventional functions form inputs to outputs. We have applied these techniques to complex functional data structures, out of core database algorithms, as well as numerical computations.

Bio: Viktor Kuncak is Associate Professor in the School of Computer and Communication Sciences of the Swiss Federal Institute of Technology, Lausanne. His research goal is to increase software development productivity and software reliability through new algorithms and tools for synthesis, analysis, and automated reasoning. In 2012 he received an ERC grant to develop the concept of Implicit Programming, whose aim to make programming easier and more accessible. He also received a SIGSOFT distinguished paper award and his work was also published as a Communications of ACM Research Highlight. He has been a program chair of the conferences Verification, Model Checking and Abstract Interpretation (2012), as well as Formal Methods in Computer-Aided Design (2014).