|
CS Faculty Talks Date: Wednesday, 9 October 2024 Time: 12:00 - 12:50 PM Venue: Seminar Hall Automated Property Directed Self Composition (PDSC) Mandayam Srivas Chennai Mathematical Institute. 09-10-24 Abstract We consider the problem of verifying k-safety properties of a sequential program, properties that refer to k interacting executions of a program. One approach to this problem is self-composition which reduces the problem to standard 1-safety verification of the propety on a program that executes the individual steps of k-copies of the original program in some interleaved or concurrent order. The complexity of inductive invariants required for verifying the composed program depends on the quality of the composition. The problem of constructing a suitably self- composed program that can be verified with simple inductive invariants that can be automatically derived is useful and interesting. A recent work (by others) in CAV 2019 developed a technique (PDSC) by using ideas from predicate abstraction to construct a self composition along with an inductive invariant that could verify a given k-safety property. A limitation of that work is that it relies on the user to supply a set of state predicates to express the invariants in and can successfully com- plete the proof only if one exists in a language of the predicates. Our work automates PDSC further, by discovering new predicates whenever the given set is found to be inadequate. I first give an overiew of the original PDSC algorithm. Then present three different approaches or our work for obtaining new predicates - relying on syntax-guided syn- thesis (SyGUS), quantifier elimination (QE), and interpolation - and discuss the strengths and limitations of these. This is joint work with a number of people including 3 alumni of CMI. This was published in ATVA2023.
|
