User:Vkuncak
Viktor Kunčak
[edit]
|
Viktor Kunčak | |
|---|---|
 Viktor Kunčak | |
| Born | |
| Alma mater | Massachusetts Institute of Technology, University of Novi Sad |
| Known for | software synthesis and verification |
| Awards | ACM SIGSOFT distinguished paper award. Communications of the ACM Research Highlight |
| Scientific career | |
| Fields | Formal verification, Programming languages |
| Institutions | École Polytechnique Fédérale de Lausanne, Massachusetts Institute of Technology, Microsoft Research |
| Thesis | Modular Data Structure Verification (2007) |
| Doctoral advisor | Martin C. Rinard |
| Doctoral students | Ruzica Piskac (2011); Philippe Suter (2012); Hossein Hojjat (2013); Giuliano Losa (2014); Eva Darulova (2014); Tihomir Gvero (2015); Etienne Kneuss (2016); Régis Blanc (2017); Ravichandhran Kandhadai Madhavan (2017); Mikaël Mayer (2017); Nicolas Voirol (2019); Emmanouil Koukoutos (2019); Romain Edelmann (2021); Georg S. Schmid (2022), Rodrigo Raya (2023) |
Viktor Kunčak (born 1977) is an Associate Professor with tenure in the School of Computer and Communication Sciences at EPFL where he leads the research group Laboratory for Automated Reasoning and Analysis. He joined EPFL as a tenure-track assistant professor in 2007 and received tenure in 2012.
Among his main projects are the Stainless verification system, which is available on GitHub and can prove correctness or find errors in programs written in the Scala programming language.
Education
[edit]He received a PhD degree from the EECS department of the Massachusetts Institute of Technology in 2007 under the supervision of Martin C. Rinard with the dissertation [Modular Data Structure Verification]. His thesis committee members also included Arvind and Daniel Jackson. His dissertation describes some of the techniques and results of a program verifier for a subset of Java and specifications expressed in a subset of the classical Higher-order logic logic of Isabelle (proof assistant), including decision procedures and techniques to combine decision procedures. He previously received MSc degree from the EECS department of the Massachusetts Institute of Technology in 2001, also under the supervision of Martin C. Rinard.
His BSc degree is from the Department of Mathematics and Informatics in the Faculty of Sciences at the University of Novi Sad, where he worked with professors Silvia Ghilezan and Mirjana Ivanović.
Activities
[edit]Research Output
[edit]His entry in the DBLP database lists at least 104 conference publications and 22 journal publications. His Google Scholar profile indicates an H-index of at least 43.
Collaborative and Organizational Activities
[edit]He was a founding member and an initial leader of an international COST Action Rich Model Toolkit aiming to establish standardized formats for verification and synthesis.
In 2011, he organized Summer Research Institute at EPFL hosting several prominent guests in the area of verification, such as J Strother Moore and Tony Hoare.
In 2014 he was a program co-chair and local organization chair of Conference on Formal Methods in Computer-Aided Design (FMCAD). In 2017 he was a co-chair, with Rupak Majumdar, of the International Conference on Computer Aided Verification held in Heidelberg.
Teaching
[edit]He has been involved in teaching undergraduate and graduate courses at EPFL, including courses on functional programming, compiler construction, verification, and synthesis, and co-authored the parallel programming course on Coursera, which, according to Coursera, has been followed by over 50'000 learners.
Activity on Wikipedia
[edit]He has contributed to Wikipedia since at least 2002.
Keynotes
[edit]His invited talks and tutorials include those at ASPLOS, FMCAD, Lambda Days, Scala Days, NASA Formal Methods, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT.
Recognition
[edit]- ACM SIGSOFT distinguished paper award, for [Test generation through programming in UDITA], joint work with Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, and Darko Marinov
- [Software Synthesis Procedures] published in the Communications of the ACM as a Research Highlight article