38 citations · 73 across the 10 of their papers we have counts for
10 papers
Ceci n'est pas une pipe: AI systems as semantic abstractions
Jade Alglave, Patrick Cousot
An AI system's output is not the fact or world state it appears to describe, but rather an engineered representation. We propose a semantic framework to describe AI systems, to be…
I hope we don't do to trust what advertising has done to love
Jade Alglave
Advertising uses love to sell stuff, like nylons. It also uses the word "love" in trivialising ways -- do you "love" your oven? When I hear about trust in the context of AI, especi…
Syntax and semantics of the weak consistency model specification language cat
Jade Alglave, Patrick Cousot, Luc Maranget
We provide the syntax and semantics of the cat language, a domain specific language to describe consistency properties of parallel/distributed programs. The language is implemented…
Syntax and analytic semantics of LISA
Jade ALglave, Patrick Cousot
We provide the syntax and semantics of the LISA (for "Litmus Instruction Set Architecture") language. The parallel assembly language LISA is implemented in the herd7 tool (http://v…
Proceedings Eighth International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software
Simon Gay, Jade Alglave
PLACES 2015 (full title: Programming Language Approaches to Concurrency- and Communication-Centric Software) is the eighth edition of the PLACES workshop series. After the first PL…
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…