[pl-seminar] SPIN practice talks Monday 6/15 at 10 am

[Nicholas Kidd <kidd@xxxxxxxxxxx>]

On Monday 6/15 at 10am in room 3310,
there will be two back-to-back practice talks for SPIN 2009.
The format is a 25 minute presentation followed by 5 minutes for questions.

--------------------------------------------------------------------------
Title   :  Symbolic Analysis via Semantic Reinterpretation

Authors :  Junghee Lim, Akash Lal, and Thomas Reps

Abstract:
The paper presents a novel technique to create implementations of the 
basic primitives used in symbolic program analysis: forward symbolic 
evaluation, weakest liberal precondition, and symbolic composition. We 
used the technique to create a system in which, for the cost of writing 
just one specification—an interpreter for the programming language of 
interest—one obtains automaticallygenerated, mutually-consistent 
implementations of all three symbolic-analysis primitives. This can be 
carried out even for languages with pointers and address arithmetic. Our 
implementation has been used to generate symbolic-analysis primitives 
for x86 and PowerPC.
--------------------------------------------------------------------------


--------------------------------------------------------------------------
Title   :  A Decision Procedure for Detecting Atomicity Violations for 
Communicating Processes with Locks
Authors :  Nicholas Kidd, Peter Lammich, Tayssir Touili and Thomas Reps

Abstract:
We present a new decision procedure for detecting property violations in 
pushdown models for concurrent programs that use lock-based 
synchronization, where each thread’s lock operations are properly nested 
(a la synchronized methods in Java). The technique detects violations 
expressed as indexed phase automata (PAs)—a class of non-deterministic 
finite automata in which the only loops are self-loops. Our interest in 
PAs stems from their ability to capture atomic-set serializability 
violations. (Atomic-set serializability is a relaxation of atomicity to 
only a user-specified set of memory locations.) We implemented the 
decision procedure and applied it to detecting 
atomic-set-serializability violations in models of concurrent Java 
programs. Compared with a prior method based on a semi-decision 
procedure, not only was the decision procedure 7.5X faster overall, but 
the semi-decision procedure timed out on about 68% of the queries versus 
4% for the decision procedure.
--------------------------------------------------------------------------

Thanks,
Nick