Languages

Home

Workshop on Proof Assistants in Formal Methods

August 21, 2011. Suzhou, China

The workshop is part of the 3rd Asian-Pacific Summer School on Formal Methods, which will be held on August 13-21 in Suzhou, China (see http://kyhcs.ustcsz.edu.cn/fmschool-2011 ). It will be on the last day (Aug. 21) of the summer school.

The goal of the workshop is to bring together researchers using mechanized logic and proof assistants (Coq, Isabelle, HOL, PVS, etc.) in formal methods. Topics for contributed talks include, but are not limited to, the following:

  • Verification of programs, algorithms or protocols;
  • Programming language semantics;
  • Formalization of logical systems or mathematical concepts in a mechanized logic;
  • Experiences on using proof assistants in education or research projects;
  • New development and contributions of proof assistants, including theories, tactics, libraries, interfacing different verification systems, etc.;

This informal workshop aims at a high degree of useful interaction amongst the participants, welcoming proposals for talks on work in progress, overviews of larger programs, position presentations and short tutorials as well as more traditional research talks describing new results. Talk proposals can be submitted either in the forms of a short abstract or a longer (published or unpublished) paper. There will be NO official proceedings published for the workshop.

We will try to accommodate as many talks as possible, but, depending on the number of submissions, there might be a selection process. Note that participants of the workshop are not required to attend the summer school. Presentations need to be given in English.

Important Dates:

  • Submission deadline: July 10 (submissions should be sent to kyhcs@ustc.edu.cn )
  • Author notification: July 15
  • Workshop: August 21

Preliminary Program:

9:00-10:00   : Some experiments with Coq at LIAMA, Jean-Francois Monin (LIAMA)
10:00-10:30 : tea break
10:30-11:15 : Formalizing of Timed Petri Net using PVS*, Qingguo XU(Shanghai University)
11:15-12:00 : Verifying Thread Management by Treating Threads as Resources, Yu GUO (USTC)
12:00-2:00   : lunch (Participants of the Coq school will get meal tickets. For participants of the workshop only, the lunch will be arranged.)
2:00-2:45     : Certified Translation from Synchronous Data-Flow Languages to Imperative Procedural Languages, Zhen CAO (Tsinghua University)
2:45-3:30     : A Certifying Compiler for Clike Programming Language, Zhaopeng Li (USTC)
3:30-4:15     : Constructing the Complex Numbers in HOL4, Liming Li (Capital Normal University)

For more information, please send emails to kyhcs@ustc.edu.cn .