View source for User:Vkuncak

== Viktor Kunčak ==

{{Boxboxtop}}
{{User academic}}
{{User Computer Scientist}}
{{User teacher university}}
{{user degree/PhD}}
{{Boxboxbottom}}

{{Infobox scientist
|name              = Viktor Kunčak
|image             = [[File:Kuncak-crop2-2013-07-29.jpg|thumb]]
|image_size        = 
|caption           = Viktor Kunčak
|birth_place       = [[Novi Sad]]
|death_date        = 
|death_place       = 
|workplaces        = [[École Polytechnique Fédérale de Lausanne]], [[Massachusetts Institute of Technology]], [[Microsoft Research]]
|field             = [[Formal verification]], [[Programming languages]]
|alma_mater        = [[Massachusetts Institute of Technology]], [[University of Novi Sad]]
|doctoral_advisor  = Martin C. Rinard
|thesis_title     = [http://hdl.handle.net/1721.1/38533 Modular Data Structure Verification]
|thesis_year      = 2007
|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)
|known_for         = software synthesis and verification
|author_abbrev_bot = 
|author_abbrev_zoo = 
|influences        = 
|influenced        = 
|prizes            = ACM SIGSOFT distinguished paper award. [[Communications of the ACM]] Research Highlight
|religion          = 
|footnotes         = 
}}

'''Viktor Kunčak''' (born 1977) is an Associate Professor with tenure in the [http://ic.epfl.ch School of Computer and Communication Sciences] at [[EPFL]] where he leads the research group [http://lara.epfl.ch 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 [https://stainless.epfl.ch/ Stainless verification system], which is [https://github.com/epfl-lara/stainless available on GitHub] and can prove correctness or find errors in programs written in the [[Scala programming language]].

=== Education ===

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 [[http://hdl.handle.net/1721.1/38533 Modular Data Structure Verification]]. His thesis committee members also included [[Arvind_(computer_scientist)|Arvind]] and [[Daniel_Jackson_(computer_scientist)|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 ===

==== Research Output ====

His [https://dblp.org/pid/k/ViktorKuncak.html entry] in the [[DBLP|DBLP database]] lists at least 104 conference publications and 22 journal publications. 
His [https://scholar.google.com/citations?user=kmoklesAAAAJ&hl=en&oi=ao Google Scholar profile] indicates an [[H-index]] of at least 43.

==== Collaborative and Organizational Activities ====

He was a founding member and an initial leader of an international [http://richmodels.epfl.ch COST Action Rich Model Toolkit] aiming to establish standardized formats for [[Verification and validation (software)|verification]] and synthesis.

In 2011, he organized [http://suri.epfl.ch/past/2011 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 ====

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 [https://www.coursera.org/learn/scala-parallel-programming parallel programming course] on [[Coursera]], which, according to Coursera, has been followed by over 50'000 learners.

==== Activity on Wikipedia ====

He [[Special:Contributions/Vkuncak|has contributed to Wikipedia]] since at least 2002.

==== Keynotes ====

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 ===

* ACM SIGSOFT distinguished paper award, for [[http://dx.doi.org/10.1145/1806799.1806835 Test generation through programming in UDITA]], joint work with 	Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, and Darko Marinov
* [[http://dx.doi.org/10.1145/2076450.2076472 Software Synthesis Procedures]] published in the Communications of the ACM as a Research Highlight article

=== Links ===

* [https://www.genealogy.math.ndsu.nodak.edu/id.php?id=127834 Viktor Kuncak] at the [[Mathematics Genealogy Project]]
* [http://lara.epfl.ch/~kuncak Viktor Kuncak's home page] at [[École Polytechnique Fédérale de Lausanne|EPFL]]
* [http://lara.epfl.ch/~kuncak/cv.pdf CV of Viktor Kuncak]
* [http://lara.epfl.ch Lab for Automated Reasoning and Analysis]