REMS-DeepSpec 2020 Contributors - REMS-DeepSpec 2020

Filter

Role Type

Contributing to

Number of Roles

Country

Results (70)

A Andrew AppelAppel, Andrew Princeton Verified Software Toolchain: a powerful and practical tool
Alasdair ArmstrongArmstrong, Alasdair University of Cambridge Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
Alasdair ArmstrongArmstrong, Alasdair University of Cambridge ARMv8 and RISC-V relaxed memory concurrency
Sacha-Élie AyounAyoun, Sacha-Élie Imperial College London, UK Gillian: a Multi-language Platform for Program Correctness and Incorrectness
B Guillaume BarbierBarbier, Guillaume ENS Rennes, France WebAssembly: sequential and concurrent semantics
Thomas BauereissBauereiss, Thomas University of Cambridge Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM} Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States Welcome and brief project overviews Committee Member in Organizing Committee within the REMS-DeepSpec-track
Martin BodinBodin, Martin Imperial College LondonUnited Kingdom WebAssembly: sequential and concurrent semantics
C Brian CampbellCampbell, Brian University of Edinburgh Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM} Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
Sunjay CauligiCauligi, Sunjay University of California at San Diego, USA WebAssembly: sequential and concurrent semantics
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System
Joonwon ChoiChoi, Joonwon Massachusetts Institute of Technology, USA The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System
D Will DeaconDeacon, Will ARM Ltd. ARMv8 and RISC-V relaxed memory concurrency
Dominique DevrieseDevriese, Dominique Vrije Universiteit BrusselBelgium Katamaran: semi-automated verification of ISA specifications
Craig DisselkoenDisselkoen, Craig University of California at San Diego, USA WebAssembly: sequential and concurrent semantics
Stephen DolanDolan, Stephen University of Cambridge, UK WebAssembly: sequential and concurrent semantics
E Andres ErbsenErbsen, Andres The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System
F Shaked FlurFlur, Shaked Google Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V ARMv8 and RISC-V relaxed memory concurrency WebAssembly: sequential and concurrent semantics
Anthony FoxFox, Anthony University of Cambridge, UK Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
Jon FrenchFrench, Jon University of Cambridge Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V ARMv8 and RISC-V relaxed memory concurrency
G Philippa GardnerGardner, Philippa Imperial College London, UK Gillian: a Multi-language Platform for Program Correctness and Incorrectness WebAssembly: sequential and concurrent semantics
Tal GarfinkelGarfinkel, Tal Stanford University WebAssembly: sequential and concurrent semantics
Victor B. F. GomesGomes, Victor B. F. University of Cambridge, UK Cerberus: executable reference semantics and memory object models for ISO and de facto C
Kathryn E. GrayGray, Kathryn E. FacebookUnited Kingdom Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V ARMv8 and RISC-V relaxed memory concurrency
Samuel GruetterGruetter, Samuel Massachusetts Institute of Technology The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System
Shu-yu GuoGuo, Shu-yu Bloomberg, USA WebAssembly: sequential and concurrent semantics
H Chung-Kil HurHur, Chung-Kil Seoul National University, South Korea ARMv8 and RISC-V relaxed memory concurrency
J Alexandre JoannouJoannou, Alexandre University of CambridgeUnited Kingdom Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
K Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom ARMv8 and RISC-V relaxed memory concurrency
Jeehoon KangKang, Jeehoon KAISTSouth Korea ARMv8 and RISC-V relaxed memory concurrency
Steven KeuchelKeuchel, Steven Katamaran: semi-automated verification of ISA specifications
Neel KrishnaswamiKrishnaswami, Neel Computer Laboratory, University of Cambridge Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V WebAssembly: sequential and concurrent semantics Committee Member in Program Committee within the REMS-DeepSpec-track
L Stella LauLau, Stella Cerberus: executable reference semantics and memory object models for ISO and de facto C
Sung-Hwan LeeLee, Sung-Hwan Seoul National University, South KoreaSouth Korea ARMv8 and RISC-V relaxed memory concurrency
Amit LevyLevy, Amit WebAssembly: sequential and concurrent semantics
Georgy LukyanovLukyanov, Georgy Newcastle University, UKUnited Kingdom Katamaran: semi-automated verification of ISA specifications
M Petar MaksimovićMaksimović, Petar Imperial College London, UK Gillian: a Multi-language Platform for Program Correctness and Incorrectness WebAssembly: sequential and concurrent semantics
Luc MarangetMaranget, Luc Inria ParisFrance ARMv8 and RISC-V relaxed memory concurrency
Justus MatthiesenMatthiesen, Justus University of Cambridge Cerberus: executable reference semantics and memory object models for ISO and de facto C
Kayvan MemarianMemarian, Kayvan University of CambridgeIran Cerberus: executable reference semantics and memory object models for ISO and de facto C
Simon W. MooreMoore, Simon W. University of Cambridge Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
Prashanth MundkurMundkur, Prashanth SRI International Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology, SwedenSweden Committee Member in Program Committee within the REMS-DeepSpec-track
N Matthew NaylorNaylor, Matthew University of CambridgeUnited Kingdom Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
Peter G. NeumannNeumann, Peter G. SRI InternationalUnited States Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
Kyndylan NienhuisNienhuis, Kyndylan University of Cambridge Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
Robert M. NortonNorton, Robert M. University of Cambridge Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM} Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
P Jean Pichon-PharabodPichon-Pharabod, Jean University of Cambridge, UK ARMv8 and RISC-V relaxed memory concurrency Cerberus: executable reference semantics and memory object models for ISO and de facto C WebAssembly: sequential and concurrent semantics
Anton PodkopaevPodkopaev, Anton MPI-SWS, NRU HSE, JetBrains ResearchRussia WebAssembly: sequential and concurrent semantics
Natalie PopescuPopescu, Natalie University of California San Diego WebAssembly: sequential and concurrent semantics
Christopher PultePulte, Christopher University of Cambridge, UK Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V ARMv8 and RISC-V relaxed memory concurrency WebAssembly: sequential and concurrent semantics
R Alastair ReidReid, Alastair Google ResearchUnited Kingdom Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
John RennerRenner, John University of California at San Diego, USA WebAssembly: sequential and concurrent semantics
Michael RoeRoe, Michael University of CambridgeUnited Kingdom Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
Andreas RossbergRossberg, Andreas Dfinity StiftungGermany WebAssembly: sequential and concurrent semantics
S José Fragoso SantosSantos, José Fragoso Imperial College London Gillian: a Multi-language Platform for Program Correctness and Incorrectness
Susmit SarkarSarkar, Susmit University of St. Andrews ARMv8 and RISC-V relaxed memory concurrency
Peter SewellSewell, Peter University of Cambridge Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM} Welcome and brief project overviews Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V ARMv8 and RISC-V relaxed memory concurrency Cerberus: executable reference semantics and memory object models for ISO and de facto C Committee Member in Organizing Committee within the REMS-DeepSpec-track
Ali SezginSezgin, Ali University of Cambridge ARMv8 and RISC-V relaxed memory concurrency
Ji-Yong ShinShin, Ji-Yong Yale UniversityUnited States Compositional Atomic Distributed Object Specifications for Distributed System Verification
Ben SimnerSimner, Ben ARMv8 and RISC-V relaxed memory concurrency
Ian StarkStark, Ian The University of EdinburghUnited Kingdom Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM} Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
Deian StefanStefan, Deian University of California at San Diego, USA WebAssembly: sequential and concurrent semantics
T Joseph TassarottiTassarotti, Joseph Boston College Verifying Crash-Safe, Concurrent Systems with Perennial
W Mark WassellWassell, Mark University of Cambridge Sail: ISA semantics, symbolic execution, and axiomatic concurrency for ARMv8-A and RISC-V
Robert N. M. WatsonWatson, Robert N. M. University of Cambridge Rigorous modelling and proof for system security engineering: verifying whole-ISA security properties of CHERI-{MIPS,RISC-V,ARM}
Conrad WattWatt, Conrad University of Cambridge, UK WebAssembly: sequential and concurrent semantics
X Rao XiaojXiaoj, Rao Imperial CollegeUnited Kingdom WebAssembly: sequential and concurrent semantics
Z Yannick ZakowskiZakowski, Yannick University of Pennsylvania Representing recursive and impure programs in Coq: from a toy assembly language to a modular formal semantics for LLVM IR
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Committee Member in Program Committee within the REMS-DeepSpec-track