ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sat 6 Apr 2019 14:30 - 15:00 at JUPITER - Afternoon A

In this talk, I will cover a line of work (done jointly with Mooly and several other collaborators) that originated from TVLA and its application to verifying concurrent programs, but then took a different direction. I will talk about concurrency control protocols, and their usefulness in ensuring serializability. Shifting from an analysis and verification perspective, I will talk about use of synthesis to achieve correct-by-construction software (from a concurrency control perspective). I will discuss problems such as extending a sequential object to be a linearizable object, extending a linearizable object to be a transactional object, and composing multiple transactional objects into a single transactional object.

Sat 6 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
Afternoon AMooly Fest at JUPITER
14:00
30m
Talk
Proofs and Counterexamples
Mooly Fest
Neil Immerman University of Massachusetts, Amherst
14:30
30m
Talk
Concurrency Control Contract Composition
Mooly Fest
G. Ramalingam Microsoft Research
15:00
30m
Talk
Special Relations for Special Relationships
Mooly Fest
Nikolaj Bjørner Microsoft Research