ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 15:30 - 16:00 at JUPITER - Software Verification II Chair(s): Heike Wehrheim

Verifying whether a procedure is observationally pure is useful in many software engineering scenarios. An observationally pure procedure always returns the same value for the same argument, and thus mimics a mathematical function. The problem is challenging when procedures use private mutable global variables, e.g., for memoization of frequently returned answers, and when they involve recursion. We present a novel verification approach for this problem. Our approach involves encoding the procedure’s code as a formula that is a disjunction of path constraints, with the recursive calls being replaced in the formula with references to a mathematical function symbol. Then, a theorem prover is invoked to check whether the formula that has been constructed agrees with the function symbol referred to above in terms of input-output behavior for all arguments. We evaluate our approach on a set of realistic examples, using the Boogie intermediate language and theorem prover. Our evaluation shows that the invariants are easy to construct manually, and that our approach is effective at verifying observationally pure procedures.

Wed 10 Apr

fase-2019-papers
14:00 - 16:00: FASE 2019 - Software Verification II at JUPITER
Chair(s): Heike WehrheimPaderborn University
fase-2019-papers14:00 - 14:30
Talk
Link to publication
fase-2019-papers14:30 - 15:00
Talk
Aleksandar S. DimovskiMother Teresa University, Skopje, Axel LegayINRIA Rennes, Andrzej WąsowskiIT University of Copenhagen, Denmark
Link to publication
fase-2019-papers15:00 - 15:30
Talk
Huang Li, Eun-Young KangUniversity of Southern Denmark
Link to publication
fase-2019-papers15:30 - 16:00
Talk
Himanshu Arora, Raghavan KomondoorIndian Institute of Science, Bangalore, G. RamalingamMicrosoft Research
Link to publication