Category Talks

We introduce transactions into libraries of concurrent data structures; such transactions can be used to ensure atomicity of sequences of data structure operations. By focusing on transactional access to a well-defined set of data structure operations, we strike a balance…

Leslie Lamport will answer questions regarding his Heidelberg Laureate Forum lecture.

Workers in forests: developments in parallel decision diagrams

Rigorous System Design in BIP

Reasoning about Interference (or Lack Thereof)

An Algebra of Modular Systems

Markov chains and Markov decision processes in Isabelle/HOL

A Formal Study of Collaborative Access Control in Distributed Datalog