Workshop on Realistic Program Verification

Program verification is a very attractive research area that is slowly becoming more mainstream and applied to realistic programming languages and industrially sized problems. This workshop brings together researchers in the Netherlands with international researchers in this field.

The workshop will take place on 2 December at the Radboud University Nijmegen, the day after the PhD defense of Robbert Krebbers, whose thesis is on a formalization of the C standard in Coq.

Registration

Registration is required, but free of charge. Please visit this link to register.

Program

10:00 – 10:45
Xavier Leroy
Verasco: Formal verification of a C static analyzer based on abstract interpretation

10:50 – 11:35
Wouter Swierstra
Semantics of version control

13:10 – 13:55
Lars Birkedal
Higher-Order Concurrent Separation Logic: Why and How

14:00 – 14:45
Yves Bertot
Structuring mathematical proofs: an example on multivariate polynomials and proofs of transcendence

15:15 – 16:00
Robbert Krebbers
Formalization of C: What we have learned and beyond

Organizers

Herman Geuvers (Radboud University, The Netherlands)
Robbert Krebbers (Aarhus University, Denmark)
Freek Wiedijk (Radboud University, The Netherlands)