Jade Alglave

37 papers A* 12A 2B 4Journal 16Unranked 2
YearRankTypeTitle / Venue / Authors
2024 J jnl
Puss in Boots: Formalizing Arm's Virtual Memory System Architecture.
IEEE Micro
Jade Alglave, Richard Grisenthwaite, Artem Khyzha, Luc Maranget, Nikos Nikoleris
2021 J jnl
Armed Cats: Formal Concurrency Modelling at Arm.
ACM Trans. Program. Lang. Syst.
Jade Alglave, Will Deacon, Richard Grisenthwaite, Antoine Hacquard, Luc Maranget
2018 A* conf
Frightening Small Children and Disconcerting Grown-ups: Concurrency in the Linux Kernel.
ASPLOS
Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, Alan S. Stern
2017 B conf
Coalition, intrigue, ambush, destruction and pride: Herding cats can be challenging.
FMCAD
Jade Alglave
2017 J jnl
Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion.
ACM Trans. Program. Lang. Syst.
Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl
2017 A* conf
Ogre and Pythia: an invariance proof method for weak consistency models.
POPL
Jade Alglave, Patrick Cousot
2016 J jnl
Concurrency with Weak Memory Models (Dagstuhl Seminar 16471).
Dagstuhl Reports
Jade Alglave, Patrick Cousot, Caterina Urban
2016 — ed.
Proceedings Eighth International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2015, London, UK, 18th April 2015.
PLACES
Simon Gay, Jade Alglave
2016 B conf
Simulation and Invariance for Weak Consistency.
SAS
Jade Alglave
2016 J jnl
Syntax and analytic semantics of LISA.
CoRR
Jade Alglave, Patrick Cousot
2016 J jnl
Syntax and semantics of the weak consistency model specification language cat.
CoRR
Jade Alglave, Patrick Cousot, Luc Maranget
2015 A* conf
GPU Concurrency: Weak Behaviours and Programming Assumptions.
ASPLOS
Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, John Wickerson
2015 J jnl
I compute, therefore I am (buggy): methodic doubt meets multiprocessors.
Tiny Trans. Comput. Sci.
Jade Alglave, Luc Maranget, Daniel Poetzl, Tyler Sorensen
2015 — conf
Modeling of Architectures.
SFM
Jade Alglave
2015 J jnl
New Lace and Arsenic: adventures in weak memory with a program logic.
CoRR
Richard Bornat, Jade Alglave, Matthew J. Parkinson
2014 J jnl
Concurrent Kleene Algebra of Partial Strings.
CoRR
Alex Horn, Jade Alglave
2014 A* conf
Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion.
CAV
Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl
2014 J jnl
Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory.
ACM Trans. Program. Lang. Syst.
Jade Alglave, Luc Maranget, Michael Tautschnig
2014 A* conf
Herding cats: modelling, simulation, testing, and data-mining for weak memory.
PLDI
Jade Alglave, Luc Maranget, Michael Tautschnig
2013 J jnl
Don't sit on the fence: A static analysis approach to automatic fence insertion.
CoRR
Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl
2013 J jnl
Herding Cats.
CoRR
Jade Alglave, Luc Maranget, Michael Tautschnig
2013 J jnl
Partial Orders for Efficient BMC of Concurrent Software
CoRR
Jade Alglave, Daniel Kroening, Michael Tautschnig
2013 A* conf
Partial Orders for Efficient Bounded Model Checking of Concurrent Software.
CAV
Jade Alglave, Daniel Kroening, Michael Tautschnig
2013 A conf
Software Verification for Weak Memory via Program Transformation.
ESOP
Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig
2012 J jnl
A formal hierarchy of weak memory models.
Formal Methods Syst. Des.
Jade Alglave
2012 A* conf
An Axiomatic Memory Model for POWER Multiprocessors.
CAV
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, Derek Williams
2012 J jnl
Fences in weak memory models (extended version).
Formal Methods Syst. Des.
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell
2012 J jnl
Software Verification for Weak Memory via Program Transformation
CoRR
Jade Alglave, Daniel Kroening, Vincent Nimal, Michael Tautschnig
2012 A* conf
Synchronising C/C++ and POWER.
PLDI
Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams
2011 A conf
Litmus: Running Tests against Hardware.
TACAS
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell
2011 B conf
Making Software Verification Tools Really Work.
ATVA
Jade Alglave, Alastair F. Donaldson, Daniel Kroening, Michael Tautschnig
2011 B conf
Soundness of Data Flow Analyses for Weak Memory Models.
APLAS
Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, Michael Tautschnig
2011 A* conf
Stability in Weak Memory Models.
CAV
Jade Alglave, Luc Maranget
2011 A* conf
Understanding POWER multiprocessors.
PLDI
Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams
2010 A* conf
Fences in Weak Memory Models.
CAV
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell
2009 — conf
The semantics of power and ARM multiprocessor machine code.
DAMP
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli
2009 A* conf
The semantics of x86-CC multiprocessor machine code.
POPL
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave