PSPL 2010: Papers with Abstracts

Papers
A simple proof system for lock-free concurrency Luís Caires, Carla Ferreira and António Ravara Abstract. Concurrent algorithms classically relied on locks to guarantee the absence of interference when accessing shared resources. The massive use of distributed systems and of new multi-core architectures makes this approach unfeasible, and novel techniques are needed. Lock-Free algorithms have thus gained momentum. We define a core imperative calculus, equipped with concurrency and low level lock-free synchronization primitives, based on the Load-Link/Store-Conditional model. We propose a Hoare-Separation-style system to prove correct lock-free algorithms implemented in this language. Judgements distinguish local from global state, transfering knowledge between the worlds in the rules for loading and copying variables. We present a simple yet illustrative example of a proof for a concurrent data structure.
A Developer-oriented Hoare Logic Holger Gast Abstract. We present a Hoare logic and verification system designed to be understandable by developers. We discuss both the underlying considerations on the design of the system, and the formal and technical background of the tools. We show that the goals have been achieved by typical examples.
A Proof System for Reasoning about Probabilistic Concurrent Processes Matteo Mio Abstract. A Proof System for Reasoning about Probabilistic Concurrent Processes
Towards a Cut-free Sequent Calculus for Boolean BI Sungwoo Park and Jonghyun Park Abstract.
A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network Giuseppe Primiero Abstract. In the present paper we explore the use of a newly formulated polymorphic modal type theory for a computational interpretation of programs in the context of distributed processing. The initial language define judgemental modalities with a the standard constructor for necessity interpreted as the presentation of instructions for a program terminating at runtime and an independent constructor for the possibility judgement as a representation of a process of partial evaluation. In order to interpret distributed and localised computing, we propose an extension in terms of multi-modalities, to express programs equipped with locations and data accessibility. Besides localised accessibility formalised by the different signed modalities, we develop further the language by prioritising these modalities, which implement seriality or staging annotations in the program structure.
Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic Nikolay V. Shilov Abstract. Propositional Linear Temporal Logic (PLTL) is a very popular formalism for specification and verification of computer programs and systems. This extended abstract sketches a tableau-like axiomatization for PLTL based on automata-theoretic decision procedure coupled with tableau for local model checking of the propositional μ-Calculus.