38 citations · 73 across the 10 of their papers we have counts for
5 papers · 1 filter
New Lace and Arsenic: adventures in weak memory with a program logic
Richard Bornat, Jade Alglave, Matthew Parkinson
We describe a program logic for weak memory (also known as relaxed memory). The logic is based on Hoare logic within a thread, and rely/guarantee between threads. It is presented v…
Concurrent Kleene Algebra of Partial Strings
Alex Horn, Jade Alglave
Concurrent Kleene Algebra (CKA) is a recently proposed algebraic structure by Hoare and collaborators that unifies the laws of concurrent programming. The unifying power of CKA res…
Don't sit on the fence: A static analysis approach to automatic fence insertion
Jade Alglave, Daniel Kroening, Vincent Nimal +1
Modern architectures rely on memory fences to prevent undesired weakenings of memory consistency. As the fences' semantics may be subtle, the automation of their placement is highl…
Partial Orders for Efficient BMC of Concurrent Software
Jade Alglave, Daniel Kroening, Michael Tautschnig
The vast number of interleavings that a concurrent program can have is typically identified as the root cause of the difficulty of automatic analysis of concurrent software. Weak m…
Software Verification for Weak Memory via Program Transformation
Jade Alglave, Daniel Kroening, Vincent Nimal +1
Despite multiprocessors implementing weak memory models, verification methods often assume Sequential Consistency (SC), thus may miss bugs due to weak memory. We propose a sound tr…