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

VeriFast is a verification tool for single- and multi-threaded C and Java programs annotated with preconditions and postconditions written in separation logic. To enable rich specifications, the programmer may define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates. To enable verification of these rich specifications, the programmer may write lemma functions, i.e., functions that serve only as proofs that their precondition implies their postcondition. The verifier checks that lemma functions terminate and do not have side-effects. Since neither VeriFast itself nor the underlying SMT solver need to do any significant search, verification time is predictable and low. VeriFast comes with an IDE that enables interactive annotation insertion and symbolic debugging.

So far, we have used VeriFast to experiment with novel approaches for modular specification and verification of functional correctness of fine-grained concurrent algorithms [POPL 2011], memory-safety of programs that dynamically load and unload modules [FM 2011], the interactive behavior of programs that use APIs like stdio.h or java.io [ESOP 2015], termination of programs involving dynamically bound method calls [ECOOP 2015], and deadlock-freedom of programs where threads wait for other threads in the presence of exceptions [FTfJP 2015]. Furthermore, we have used VeriFast to verify crash-freedom of Java Card software for the Belgian eID card, a Linux device driver, a C program routing packets in a home gateway, and functional correctness of the complex Multiple-Compare-and-Swap lock-free concurrent algorithm, and to participate in verification competitions, winning at VerifyThis 2012 and 2016.

VeriFast is available for download at https://people.cs.kuleuven.be/~bart.jacobs/verifast/.

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 - 16:30
Demonstration
FTfJP
Bart JacobsiMinds - Distrinet, KU Leuven
16:30 - 17:00
Talk
FTfJP
Bart JacobsiMinds - Distrinet, KU Leuven
17:00 - 17:30
Talk
FTfJP
Paola Giannini, Marco ServettoVictoria University of Wellington, Elena ZuccaUniversity of Genova
17:30 - 18:00
Talk
FTfJP
Tomoyuki AotaniTokyo Institute of Technology, Japan, Gary LeavensCentral Florida University
18:00 - 18:30
Talk
FTfJP
Sophia DrossopoulouImperial College London, James NobleVictoria University of Wellington, Mark MillerGoogle Inc., Toby MurrayUniversity of Melbourne