Speaker / Predavač : Dr. Viktor Kuncak
Title / Naslov: Automated Reasoning for Reliable Software
Abstract / Rezime:
I will present our experience with developing and using tools to prove correctness properties of software systems. Using these tools we have verified correctness of data structures such as lists, trees, and hash tables. Algorithms for deciding satisfiability of logical formulas play an important role in these approaches. I will present our work on deciding satisfiability of formulas involving sets, multisets, and cardinality operators. We show a polynomial-time reduction from satisfiability of multiset formulas to satisfiability of formulas in linear arithmetic extended with a new 'star' operator. We then show that formulas of linear arithmetic with star have polynomial-sized witnesses to satisfiability using properties of integer cones and bounds on generators of solutions of integer linear programming problems. Consequently, we prove that the satisfiability problem for multiset formulas is NP-complete, exponentially improving complexity compared to previously known algorithms. SHORT BIO: Viktor Kuncak is an assistant professor at EPFL and the leader of the research group "Laboratory for Automated Reasoning and Analysis". He works on automated methods and tools for reasoning about complex properties of software systems and designs. His work combines ideas from decision procedures, theorem proving, constraint solving, static analysis, and programming languages. Viktor Kuncak received a BSc degree in Computer Science from the University of Novi Sad and a PhD degree in Electrical Engineering and Computer Science from MIT in 2007.