Blogs (28) >>
ECOOP 2016
Sun 17 - Fri 22 July 2016 Rome, Italy
Tue 19 Jul 2016 16:30 - 17:00 at Belli - Session 4 Chair(s): Vladimir Klebanov

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 Jul
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:30
Session 4FTfJP at Belli
Chair(s): Vladimir KlebanovKarlsruhe Institute of Technology
16:00
30m
Demonstration
Tool Demonstration: The VeriFast Verification System for Java and C
FTfJP
Bart JacobsiMinds - Distrinet, KU Leuven
16:30
30m
Talk
Partial Solutions to VerifyThis 2016 Challenges 2 and 3 Using VeriFast
FTfJP
Bart JacobsiMinds - Distrinet, KU Leuven
17:00
30m
Talk
Coupling Catch Clauses with Local Declarations
FTfJP
Paola Giannini, Marco ServettoVictoria University of Wellington, Elena ZuccaUniversity of Genova
17:30
30m
Talk
Towards Modular Reasoning for Context-Oriented Programs
FTfJP
Tomoyuki AotaniTokyo Institute of Technology, Japan, Gary LeavensCentral Florida University
18:00
30m
Talk
Permission and Authority Revisited: Towards a Formalization
FTfJP
Sophia DrossopoulouImperial College London, James NobleVictoria University of Wellington, Mark MillerGoogle Inc., Toby MurrayUniversity of Melbourne