-
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--2023.
[ 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--2023.
[ 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 ]
-
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--2023.
[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--2023.
[web interface].
[ bib |
github ]
-
Sail CHERI-RISC-V instruction-set architecture (ISA)
model, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
Jessica Clarke, Nathaniel Wesley Filardo, Alexandre Joannou, Prashanth
Mundkur, Robert Norton-Wright, Alexander Richardson, Peter Rugg, and Peter
Sewell, 2019--2023.
[ 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, Prashanth Mundkur, Rishiyur S. Nikhil, Jon French,
Brian Campbell, Robert Norton-Wright, Alasdair Armstrong, Thomas Bauereiss,
Shaked Flur, Christopher Pulte, Peter Sewell, Alexander Richardson, Hesham
Almatary, Jessica Clarke, Nathaniel Wesley Filardo, Peter Rugg, and Scott
Johnson, 2014--2023.
[ bib |
project page |
github ]
-
Sail 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.
[ 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 Sewell, and Dhruv Makwana, 2019--2023.
[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--2023.
[ bib |
project page |
github ]