Prof. Viktor Kuncak(EPFL, Switzerland)
"Automating Construction of Provably Correct Software"
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
|Time:||Monday, 27.02.2014, 10:30 am|
|Place:||MPI-SWS Saarbrücken, building E1 5, room 002|
|Video:||Simultaneous video cast to MPI-SWS Kaiserslautern, room 111|