Decidable Verification of Uninterpreted Programs
17/02/2023, 3pm
Speaker
Abstract
Uninterpreted programs are sequential programs with loops and recursion written over a first order vocabulary where the constant, function and predicate symbols used are completely uninterpreted. The input to an uninterpreted program is a first order structure which also determines the semantics of such a programs. The verification question in this setting asks if an uninterpreted a program meets all its assertions on all input structures. In this talk, I will discuss the decidability boundaries for the verification question of uninterpreted programs. In general, the problem is undecidable, but becomes decidable for a sub-class, called coherent uninterpreted programs. The decidability result is tight in that slightly relaxing the coherence criteria leads to undecidability. I will then discuss how the decidability result of coherent programs segue into more general classes of programs, called k-coherent programs (k is a natural number). If time permits, I will discuss extensions to the verification question for partially interpreted programs, where the vocabulary is associated with an underlying first order theory and the inputs are those first order structures which are also models of this underlying theory.
Bio
Umang Mathur is an Assistant Professor at the National University of Singapore. He received his PhD from the University of Illinois at Urbana Champaign in 2021 and was an NTT Research Fellow at the Simons Institute for the Theory of Computing at Berkeley. His research interests lie in the use of formal methods and logic for answering design, analysis and implementation questions in programming languages, software engineering and systems.