[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.
| 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 is now open at the FLoC 2010 website.
The deadline for early registration is Monday 17th May 2010
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.
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.
Enquiries to pspl2010 @ easychair.org