"Verifying and Computing with Constraint Solvers"

 

Abstract:

We present constraint solving algorithms for proving programs correct, finding errors, generating test cases, and executing new classes of declarative programming language constructs.  Using high-level languages as the starting point, our algorithms solve constraints on algebraic data types, sets, bags, and unbounded numerical types.  Our ultimate goal is to bridge the gap between human intentions and their computational realizations, by supporting users during program construction, modification, and execution.

Bio:

Viktor Kuncak is an Assistant Professor in the School of Computer and Communication Sciences at the Swiss Federal Institute of Technology Lausanne (EPFL), where he leads the Laboratory for Automated Reasoning and Analysis. He received a PhD degree from MIT in 2007, an MSc degree from MIT in 2001, and a BSc degree from the University of Novi Sad in 2000. His research is in the area of algorithms and tools for constructing reliable computer systems. He is an initiator and the chair of the Rich Model Toolkit initiative, which gathers over 50 research groups from 20 countries and spans the areas of decision procedures, verification, analysis, synthesis, and standardized representation formats.  His work on Complete Functional Synthesis was republished as a Research Highlight in the  February 2012 issue of the Communications of the ACM.

___________________________________________________________________________