-
VIP: Verifying Real-World C Idioms with Integer-Pointer
Casts.
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers,
Derek Dreyer, and Peter Sewell.
In POPL 2022, Proc. ACM Program. Lang. 6, POPL, Article 20.
[ bib |
doi |
supplementary material |
project page |
pdf |
abstract ]
-
Cerberus-BMC: a Principled Reference Semantics and
Exploration Tool for Concurrent and Sequential C.
Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean
Pichon-Pharabod, and Peter Sewell.
In CAV 2019.
[ bib |
project page |
pdf |
abstract ]
-
Exploring C Semantics and Pointer Provenance.
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell,
Alexander Richardson, Robert N. M. Watson, and Peter Sewell.
In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 67. Also
available as ISO/IEC JTC1/SC22/WG14 N2311.
[ bib |
doi |
supplementary material |
project page |
pdf |
abstract ]
-
An operational semantics for C/C++11
concurrency.
Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell.
In OOPSLA 2016.
[ bib |
doi |
pdf |
http |
abstract ]
-
Into the depths of C: elaborating the de facto
standards.
Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis,
David Chisnall, Robert N.M. Watson, and Peter Sewell.
In PLDI 2016, PLDI 2016 Distinguished Paper award.
[ bib |
doi |
project page |
pdf |
http |
abstract ]