Brian Campbell
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 5 in the filters
on a stage with
all 14 in the filters
who talks about the same things
- Thomas Bauereiss3 talks
- Thibaut Pérami4 talks
- Angus Hammond3 talks
- Zongyuan Liu3 talks
- Peter Sewell14 talks
- Armaël Guéneau7 talks
| title | conference | date |
|---|---|---|
| ArchSem: Reusable Rigorous Semantics of Relaxed Architectures | POPL 2026 | 2026-01-11 |
A reusable framework composes ISA pseudo-code from Sail with concurrency interpreters in Rock via a freemonad of 15 algebraic effects, ingesting the full ARM… | ||
| Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…) | PLDI 2025 | 2025-06-16 |
Proves that an encapsulated C-style component running on Arm Morello maintains a mod-64 accumulator invariant against arbitrary untrusted code, by mechanising… | ||
| A CHERI C Memory Model for Verified Temporal Safety | CPP 2025 | 2025-01-20 |
Defines a CHERI C object memory model that implements a new PNVI-CHERI provenance scheme, encodes five revocation strategies, and plugs into the Cerberus… | ||
| Effectful Assembly Programming with AsmFX | HOPE 2024 | 2024-09-02 |
AsmFX proposes a six‑instruction extension (enter, do, return, exit, resume, break) plus re-enter/final-re-enter and shallow variants to implement effect… | ||
| The Morello ISA semantics, proof, and test generation | POCL 2024 | 2024-01-16 |
Formal work translates the ~62,000-line ASL Morello spec into a theorem‑prover model, generates Isabelle proofs that check a monotonicity theorem (software… | ||
| nothing matches | ||