The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

                  CALL FOR PARTICIPATION

        Workshop on Realistic Program Verification

  2 December, Radboud University Nijmegen, The Netherlands
    URL: http://robbertkrebbers.nl/verification_workshop

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. It will take place
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:

  http://robbertkrebbers.nl/verification_workshop

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)