• Sail Morello (CHERI Arm) instruction-set architecture (ISA) model, Arm Limited, Thomas Bauereiss, Brian Campbell, Alasdair Armstrong, Alastair Reid, and Peter Sewell, 2022. [ bib | project page | github ]
• Cerberus-BMC tool for exploring the behaviour of small concurrent C test programs with respect to an arbitrary axiomatic concurrency model, Stella Lau, Kayvan Memarian, Victor B. F. Gomes, Kyndylan Nienhuis, Justus Matthiesen, James Lingard, and Peter Sewell, 2019. [web interface]. [ bib | project page | github ]
• ArchSem, Thibaut Pérami, Zongyuan Liu, Nils Lauermann, Brian Campbell, Alasdair Armstrong, Thomas Bauereiss, and Peter Sewell, 2020--2025. [ bib | github ]
• Arm-A System Litmus Runner, Ben Simner, Ohad Kammar, Jean Pichon-Pharabod, Jasper Parish, and Peter Sewell, 2020--2025. [ bib | github ]
• Network Semantics: formal specification of TCP, UDP, and the Sockets API, Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough, 2001--2017. [ bib | project page | github ]
• The Ott tool for writing definitions of programming languages and calculi, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Joey Eremondi, Hannes Mehnert, Karl Palmskog, Thibaut Perami, Matthew Parkinson, Hannes Mehnert, kit-ty kate, Brian Campbell, Francois Pottier, Gilles Peskine, Alastair Reid, Tom Ridge, Susmit Sarkar, Rok Strniša, and Viktor Vafeiadis, 2005--2024. [ bib | project page | github ]
• Linksem: Executable semantic model for aspects of ELF linking and DWARF debug information, Dominic Mulligan, Stephen Kell, Simon Ser, Peter Sewell, Shaked Flur, Thibaut Pérami, Robert Norton, Ramana Kumar, Jonathan French, and Thomas Bauereiss, 2014--2024. [ bib | github ]
• Lem, a tool for lightweight executable mathematics, Dominic Mulligan, Thomas Bauereiss, Kathryn E. Gray, Scott Owens, Peter Sewell, Thomas Tuerk, Basile Clement, Brian Campbell, Christopher Pulte, David Sheets, Fabian Immler, Frederic Loulergue, Francesco Zappa Nardelli, Gabriel Kerneis, James Lingard, Jean Pichon-Pharabod, Justus Matthiesen, Kayvan Memarian, Kyndylan Nienhuis, Lars Hupel, Mark Batty, Michael Greenberg, Michael Norrish, Ohad Kammar, Peter Boehm, Robert Norton, Sami Mäkelä, Shaked Flur, Stephen Kell, Thibaut Pérami, Thomas Bauereiss, Thomas Williams, Victor Gomes, and emersion, 2010--2023. [ bib | project page | github ]
• CN C verification and testing tool, Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Rini Banerjee, Peter Sewell, and Neel Krishnaswami, 2023--. [ bib | github ]
• Cerberus C executable semantics and exploration tool, Kayvan Memarian, Victor B. F. Gomes, Justus Matthiesen, Peter Sewell, Kyndylan Nienhuis, Stella Lau, Jean Pichon-Pharabod, Christopher Pulte, Rodolphe Lepigre, James Lingard, Thomas Sewell, and Dhruv Makwana, 2016--2024. [web interface]. [ bib | project page | github ]
• CppMem: C/C++ memory model exploration tool, Mark Batty, Scott Owens, Jean Pichon-Pharabod, Susmit Sarkar, and Peter Sewell, 2012--2019. [web interface]. [ bib | http ]
• RMEM: Executable operational concurrency model exploration tool for ARMv8, RISC-V, Power, and x86, Susmit Sarkar, Peter Sewell, Luc Maranget, Shaked Flur, Christopher Pulte, Jon French, Ben Simner, Scott Owens, Pankaj Pawan, Francesco Zappa Nardelli, Sela Mador-Haim, Dominic Mulligan, Ohad Kammar, Jean Pichon-Pharabod, Gabriel Kerneis, Alasdair Armstrong, Thomas Bauereiss, and Jeehoon Kang, 2010--2024. [web interface]. [ bib | github ]
• Sail CHERI-RISC-V instruction-set architecture (ISA) model, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Jessica Clarke, Nathaniel Wesley Filardo, Google, Alexandre Joannou, Microsoft, Prashanth Mundkur, Robert Norton-Wright, Alexander Richardson, Peter Rugg, and Peter Sewell, 2019--2024. [ bib | project page | github ]
• Sail CHERI-MIPS instruction-set architecture (ISA) model, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Jessica Clarke, Nathaniel Filardo, Shaked Flur, Jon French, Kathryn E. Gray, Alexandre Joannou, Robert Norton-Wright, Christopher Pulte, Alexander Richardson, and Peter Sewell, 2016--2021. [ bib | project page | github ]
• Sail RISC-V instruction-set architecture (ISA) model, ahadali5000, Alasdair Armstrong, Alexander Richardson, Aril Computer Corp. (for contributions by Scott Johnson), Ben Marshall, Bicheng Yang, Bilal Sakhawat, Brian Campbell, Chris Casinghino, Christopher Pulte, Martin Berger Codasip (for contributions by Tim Hutt, Ben Fletcher), dylux, eroom1966, Google LLC (for contributions by its employees), Hesham Almatary, Jan Henrik Weinstock, Jessica Clarke, Jon French, Martin Berger, Michael Sammler, Microsoft (for contributions by Robert Norton-Wright, Nathaniel Wesley Filardo), Muhammad Bilal Sakhawat, Nathaniel Wesley Filardo, Paul A. Clarke, Peter Rugg, Peter Sewell, Philipp Tomsich, Prashanth Mundkur, Rafael Sene, Rishiyur S. Nikhil (Bluespec, Inc.), Robert Norton-Wright, Shaked Flur, Thibaut Pérami, Thomas Bauereiss, VRULL GmbH (for contributions by its employees), William McSpaddden, and Xinlai Wan, 2014--2024. [ bib | project page | github ]
• Sail Armv9.4-A, Armv9.3-A and ARMv8.5-A instruction-set architecture (ISA) models, Thomas Bauereiss, Brian Campbell, Alasdair Armstrong, Alastair Reid, Kathryn E. Gray, Anthony Fox, Peter Sewell, and Arm Limited, 2019, 2022, 2024. [ bib | project page | github ]
• The Isla symbolic evaluation engine for Sail and Isla-axiomatic exploration tool for axiomatic concurrency models, Alasdair Armstrong, Brian Campbell, Thibaut Pérami, Ben Simner, Peter Sewellb, and Dhruv Makwana, 2019--2024. [web interface]. [ bib | project page | github ]
• The Sail Instruction-Set Architecture (ISA) specification language, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Shaked Flur, Jon French, Kathryn E. Gray, Stephen Kell, Gabriel Kerneis, Neel Krishnaswami, Prashanth Mundkur, Robert Norton-Wright, Christopher Pulte, Alastair Reid, Peter Sewell, Ian Stark, and Mark Wassell, 2013--2024. [ bib | project page | github ]