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 is required, but free of charge. Please visit this link to register.
10:00 – 10:45
Verasco: Formal verification of a C static analyzer based on abstract interpretation
10:50 – 11:35
Semantics of version control
13:10 – 13:55
Higher-Order Concurrent Separation Logic: Why and How
14:00 – 14:45
Structuring mathematical proofs: an example on multivariate polynomials and proofs of transcendence
15:15 – 16:00
Formalization of C: What we have learned and beyond
Herman Geuvers (Radboud University, The Netherlands)
Robbert Krebbers (Aarhus University, Denmark)
Freek Wiedijk (Radboud University, The Netherlands)