Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Local Reasoning for Concurrency, Distribution and Web Programming
Speaker:Azalea Raad
coming from:Imperial College
Speakers Bio: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.

Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Language:English
Date, Time and Location
Date:Monday, 3 April 2017
Time:10:00
Duration:60 Minutes
Location:Kaiserslautern
Building:G26
Room:111
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
Name(s):Roslyn Stricker
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Saarbrücken
To Building:E1 5To Room:029
Meeting ID:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):

Created:
Roslyn Stricker/MPI-SWS, 03/30/2017 09:33 AM
Last modified:
Uwe Brahm/MPII/DE, 04/03/2017 07:01 AM
  • Roslyn Stricker, 03/30/2017 09:36 AM -- Created document.