Proof Systems for Program Logics

PSPL 2010

Saturday 10th July 2010, Edinburgh, UK

A LICS 2010-affiliated workshop at FLoC 2010

[Programme] | [Registration] | [Student grants] | [Proceedings] | [Programme committee]


A great variety of program logics are in use in computer science for the specification of (software and/or hardware) systems; for example: modal and temporal logics, dynamic logic, Hoare logic, separation logic, spatial logic, nominal logic, lax logic, linear logic, intuitionistic type theory, LCF. In recent years, the goal of identifying logics and classes of system for which the verification task "system satisfies specification" is decidable, and hence amenable to "model checking", has been a prominent and successful research direction. Nevertheless, the fact remains that, for many logics and classes of system of interest, the verification task is undecidable. Formal proof systems offer a general method for formal verification that can be applicable in such cases. Such proof systems need to be tailored to the program logic and verification task under consideration. They need to be powerful enough to verify interesting properties. They need to be user-friendly enough for formal verification to be a practicable enterprise. Such systems might be directed at a human user; in which case, ideally, formal proofs for correctness will be close to informal ones. Alternatively, they might be designed to facilitate automated proof search.

There is currently a resurgence in interest in proof systems for program logics from both practical and theoretical perspectives. On the practical side, a new generation of verification tools has emerged, based on applying theorem proving techniques to dedicated program logics (e.g., SLAM, Terminator, Smallfoot, SLAyer). On the theoretical side, new forms of program logic are under development (e.g., separation logic, spatial logic, nominal logic), there are new proof methods for the modular verification of concurrent code (e.g., combinations of Rely-Guarantee and separation logic), automata-theoretic model-checking techniques are being incorporated into proof systems (e.g., the "size change" method for termination, "cyclic proofs" for fixed-points), the methods of natural deduction and sequent calculus are being extended to obtain well-structured proof systems for program logics (e.g., sequent calculi for spatial logics, natural deduction for fragments of LTL and CTL*). At the same time, notable challenges remain; for example: obtaining practical proof methods for verification of timed, continuous, probabilistic, stochastic and hybrid systems; building tools capable of automatically verifying industrial-scale code.


Programme

09.00-10.00   Invited talk: Recent developments in concurrent program logics
  Viktor Vafeiadis (University of Cambridge)
 
10.00-10.30 Break
 
10.30-11.00 A simple proof system for lock-free concurrency
  Luís Caires, Carla Ferreira and António Ravara (Universidade Nova de Lisboa)
11.00-11.30 A multi-modal dependent type theory for representing data accessibility in a network
  Giuseppe Primiero (Ghent University)
11.30-12.00 Towards a Cut-free Sequent Calculus for Boolean BI
  Sungwoo Park and Jonghyun Park (Pohang University of Science and Technology)
12.00-12.30 A Developer-oriented Hoare Logic
  Holger Gast (University of Tübingen)
 
12.30-14.00 Lunch
 
14.00-15.00   Invited talk: Proof Systems for Hybrid System Logics
  André Platzer (Carnegie Mellon University)
 
15.00-15.30 Break
 
15.30-16.00 A Proof System for Reasoning about Probabilistic Concurrent Processes
  Matteo Mio (University of Edinburgh)
 
16.00-17.00 Discussion session: Challenge topics in PSPL
  Led by Peter O'Hearn and Alex Simpson


Registration

Registration is now open at the FLoC 2010 website.

The deadline for early registration is Monday 17th May 2010


Student grants

A number of grants are available for PhD students wishing to attend this workshop. For further information, please email pspl2010@easychair.org, stating "Student grants" in the subject header.


Proceedings and journal special issue

Abstracts will be included in the FLoC Workhops electronic proceedings, and in a volume of EasyChair Proceedings.

Accepted authors should submit final abstracts for the proceedings via EasyChair by midnight UST on Monday 17th May 2010

It is planned to follow the workshop with a special issue of the journal Mathematical Structures in Computer Science.


Programme committee

  • Luis Caires (Universidade Nova de Lisboa)
  • Robert Harper (Carnegie Mellon University)
  • Peter O'Hearn (Queen Mary London)
  • Dale Miller (INRIA)
  • Matthew Parkinson (Microsoft Research Cambridge)
  • Dana Scott (Carnegie Mellon University, Emeritus)
  • Alex Simpson (Edinburgh, chair)
  • Luca Vigano (Verona)

Enquiries to pspl2010 @ easychair.org