Description
Speaker: Umang Mathur (University of Illinois at Urbana-Champaign)
Title: Decidable Verification of Uninterpreted Programs
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 for each input first-order structures, the induced program execution satisfies all assertions encountered.
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 we introduce, called coherent uninterpreted programs. The decidability result is tight in that slightly relaxing the coherence criteria leads to undecidability.
Towards the end of the talk, I will briefly discuss (a) how the decidability result of coherent programs segue into more general classes of programs, called k-coherent programs (k is a natural number), and (b) extensions to the verification question for partially interpreted programs.
The slides for today's talk are here: https://www.cs.bham.ac.
The talk was based on this paper: http://umathur3.web.