-
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 ]
-
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 ]