ECOOP 2016 (series) / FTfJP 2016 (series) / FTfJP /
Partial Solutions to VerifyThis 2016 Challenges 2 and 3 Using VeriFast
We describe our partial solutions, using our VeriFast separation-logic based tool for modular formal verification of C and Java programs, to Challenges 2 and 3 of the VerifyThis 2016 Verification Competition, involving the verification of crash-freedom and certain correctness properties of code fragments implementing constant-space tree traversal and a tree barrier.
Assistant professor at the iMinds-DistriNet research group at the Department of Computer Science, KU Leuven - University of Leuven, Belgium
Tue 19 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 19 Jul
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 18:30 | |||
16:00 30mDemonstration | Tool Demonstration: The VeriFast Verification System for Java and C FTfJP Bart Jacobs iMinds - Distrinet, KU Leuven | ||
16:30 30mTalk | Partial Solutions to VerifyThis 2016 Challenges 2 and 3 Using VeriFast FTfJP Bart Jacobs iMinds - Distrinet, KU Leuven | ||
17:00 30mTalk | Coupling Catch Clauses with Local Declarations FTfJP | ||
17:30 30mTalk | Towards Modular Reasoning for Context-Oriented Programs FTfJP | ||
18:00 30mTalk | Permission and Authority Revisited: Towards a Formalization FTfJP Sophia Drossopoulou Imperial College London, James Noble Victoria University of Wellington, Mark Miller Google Inc., Toby Murray University of Melbourne | ||
