Viktor Kuncak is an associate professor in the School of Computer and Communication Sciences, where he leads the Laboratory for Automated Reasoning and Analysis (lara.epfl.ch).  He works in formal methods with emphasis on algorithms and tools. He received a PhD degree from the Massachusetts Institute of Technology (MIT) in 2007.  He was a program chair of VMCAI 2012, is a program chair of FMCAD 2014, and he led an international COST Action to establish standardized formats for verification and synthesis (Rich Model Toolkit). His invited talks include those at ICALP, CSL, RV, VMCAI, and SMT. He received an ACM SIGSOFT distinguished paper award for work on automated testing. His work on software synthesis procedures was published in the Communications of the ACM as a Research Highlight article. His recent work on Implicit Programming, funded by a European Research Council (ERC) grant, aims to bridge the gap between human goals and their computational realizations.