MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Local Reasoning for Concurrency, Distribution and Web Programming

Azalea Raad
Imperial College
SWS Colloquium

Azalea is currently a PhD student at Imperial College's Department of Computing, supervised by Philippa Gardner and Sophia Drossopoulou. She is interested in applying formal verification
techniques to web technologies, programming languages, and new application domains.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Monday, 3 April 2017
10:00
60 Minutes
G26
111
Kaiserslautern

Abstract

In this talk I will present my research in developing local reasoning techniques in both concurrent and sequential settings.

On the concurrency side, I’ll present my work on the program logic of CoLoSL (Concurrent Local Subjective Logic) and its application to various fine-grained concurrent algorithms.
A key difficulty in verifying concurrent programs is reasoning compositionally about each thread in isolation. CoLoSL is the first program logic to introduce the general composition
and framing of interference relations (describing how shared resources may be manipulated by each thread) in the spirit of resource composition and framing in separation logic.
This in turn enables local reasoning and allows for more concise specifications and proofs.

I will then present preliminary work on extending CoLoSL to reason about distributed database applications running under the snapshot isolation (SI) consistency model. SI is a
commonly used consistency model for transaction processing, implemented by most distributed databases. The existing work focuses on the SI semantics and verification techniques
for client-side applications remain unexplored. To fill this gap, I look into extending CoLoSL towards a program logic for client-side reasoning under SI.

On the sequential side, I’ll briefly discuss my work on specification and verification of web programs. My research in this area include: a compositional specification of the
DOM (Document Object Model) library in separation logic; integrating this DOM specification with the JaVerT (JavaScript Verification Toolchain) framework for automated DOM/JavaScript
client verification; as well as ongoing work towards extending JaVerT to reason about higher-order JavaScript programs.

Contact

Roslyn Stricker
--email hidden

Video Broadcast

Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only

Roslyn Stricker, 03/30/2017 09:36 -- Created document.