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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:30
Session 4FTfJP at Belli
Chair(s): Vladimir Klebanov Karlsruhe Institute of Technology
16:00
30m
Demonstration
Tool Demonstration: The VeriFast Verification System for Java and C
FTfJP
Bart Jacobs iMinds - Distrinet, KU Leuven
16:30
30m
Talk
Partial Solutions to VerifyThis 2016 Challenges 2 and 3 Using VeriFast
FTfJP
Bart Jacobs iMinds - Distrinet, KU Leuven
17:00
30m
Talk
Coupling Catch Clauses with Local Declarations
FTfJP
Paola Giannini , Marco Servetto Victoria University of Wellington, Elena Zucca University of Genova
17:30
30m
Talk
Towards Modular Reasoning for Context-Oriented Programs
FTfJP
Tomoyuki Aotani Tokyo Institute of Technology, Japan, Gary T. Leavens Central Florida University
18:00
30m
Talk
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