CS Talk – Alexander Nutz
Host: Ruzica Piskac
Please contact Ruzica if you would like to meet with the speaker.
Title: Different Maps for Different Uses - A Program Transformation for Intermediate Verification Languages
Abstract:
In theorem prover or SMT solver based verification, the program to be verified is often given in an intermediate verification language such as Boogie, Why, or CHC. This setting raises new challenges. We investigate a preprocessing step which takes the similar role that alias analysis plays in verification, except that now, a (mathematical) map is used to model the memory or a data object of type array. We present a program transformation that takes a program P to an equivalent program P’ such that, by verifying P’ instead of P, we can reduce the burden on the SMT solver that is incurred through a large number of case splits. Here, the case splits are according to whether two statements using the same map variable are independent or not; if they are independent, we might as well employ two different map variables and thus remove the need for a case split (this is the idea behind the program transformation). We have implemented the program transformation and show that, in an ideal case, we can avoid the exponential explosion in verification runtime incurred through the case splits.
Bio:
Alexander Nutz is a PhD student of computer science at the University of Freiburg, Germany, at the chair of Software Engineering led by Andreas Podelski. His main research interests lie in the field of program verification, in particular symbolic model checking and SMT solving.