Derek Dreyer -

Registered user since Sun 28 Sep 2014

Name:Derek Dreyer

Country:Germany

Affiliation:MPI-SWS

Personal website:http://www.mpi-sws.org/~dreyer

Contributions

SPLASH 2023	Author of Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning within the OOPSLA-track Associate Chair in OOPSLA Review Committee within the OOPSLA-track
POPL 2023	Author of DimSum: A Decentralized Approach to Multi-language Semantics and Verification within the POPL-track Author of Conditional Contextual Refinement within the POPL-track Moderator of Panel: Next 50 Years of POPL within the POPL-track
PLMW @ ICFP 2022	Speaker of How to Write Papers and Give Talks That People Can Follow within the PLMW @ ICFP 2022-track
SPLASH 2022	Author of Proving Hypersafety Compositionally within the OOPSLA-track Mentor in Mentors within the PLMW-track Author of BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs within the OOPSLA-track Session Chair of Semantics and Security (part of OOPSLA) Author of Finding real bugs in big programs with incorrectness logic within the OOPSLA-track
ICFP 2022	Author of Later Credits: Resourceful Reasoning for the Later Modality within the ICFP Papers and Events-track
ECOOP 2022	Committee Member in Program Committee within the Research Papers-track
PLDI 2022	Author of (PLDI 2021) Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic within the SIGPLAN Track-track Author of Islaris: Verification of Machine Code Against Authoritative ISA Semantics within the PLDI-track Author of RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code within the PLDI-track Author of Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic within the PLDI-track Author of (PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types within the SIGPLAN Track-track
Infer 2022	Author of Finding Real Bugs in Big Programs with Incorrectness Logic within the Infer 2022-track
POPL 2022	Author of VIP: Verifying Real-World C Idioms with Integer-Pointer Casts within the POPL-track Author of Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations within the POPL-track Author of Concurrent Incorrectness Separation Logic within the POPL-track
ICFP 2021	MPI-SWS in Steering Committee Author of GhostCell: Separating Permissions from Data in Rust within the Research Papers-track
PLMW @ ICFP 2021	Speaker of How to Write Papers So People Can Read Them within the PLMW @ ICFP 2021-track
PLDI 2021	Author of Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic within the PLDI-track Author of RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types within the PLDI-track
PLMW@PLDI 2021	Speaker of How to give talks that people can follow within the PLMW@PLDI 2021-track
POPL 2021	Author of Transfinite Step-Indexing for Termination within the POPL-track
ICFP 2020	Author in Steering Committee
PLMW @ ICFP 2020	Speaker of How To Write Papers So People Can Read Them within the PLMW @ ICFP 2020-track
PLDI 2020	Session Chair of Session 7 (part of Ask Me Anything)
PLMW 2020	Author of How to Write Papers So People Can Read Them within the PLMW 2020-track Invited Speaker in Invited speakers within the PLMW 2020-track
POPL 2020	Author of The High-Level Benefits of Low-Level Sandboxing within the Research Papers-track Author of Stacked Borrows: An Aliasing Model for Rust within the Research Papers-track Author of The Future is Ours: Prophecy Variables in Separation Logic within the Research Papers-track Author of RustBelt Meets Relaxed Memory within the Research Papers-track Author of [T4] Proving Semantic Type Soundness in Iris within the TutorialFest-track
SPLASH 2019	Speaker in Speakers & Panelists within the PLMW-track Speaker of How To Write Papers So People Can Read Them within the PLMW-track
PLMW @ ICFP 2019	Committee Member in Speakers within the PLMW @ ICFP 2019-track Author of How to give talks that people can follow within the PLMW @ ICFP 2019-track
ICFP 2019	General Chair in Organizing Committee Session Chair of Monday Keynote (part of Keynotes and Reports) ICFP'19 General Chair in Steering Committee
ECOOP 2019	Committee Member in Program Committee within the Research Papers-track
SPLASH 2018	Committee Member in Review Committee within the OOPSLA-track Mentor in Mentors within the Breakfasts-track
ICFP 2018	ICFP'19 General Chair in Steering Committee Author of ICFP 2019 Announcement within the Keynotes and Reports-track Author of MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic within the Research Papers-track Author of Mtac2: Typed Tactics for Backward Reasoning in Coq within the Research Papers-track
PLMW 2018	Committee Member in Speakers within the PLMW-track Author of How to Give Talks That People Can Follow within the PLMW-track
POPL 2018	Author of RustBelt: Securing the Foundations of the Rust Programming Language within the Artifact Evaluation-track Author of Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and Now You Can) within the Research Papers-track Author of RustBelt: Securing the Foundations of the Rust Programming Language within the Research Papers-track
SPLASH 2017	Author of Robust and Compositional Verification of Object Capability Patterns within the OOPSLA-track
PLMW 2017	Author of How to Write Papers and Give Talks That People Can Follow within the PLMW 2017-track
ICFP 2017	ICFP'19 General Chair in Steering Committee
HOPE 2017	Author of RustBelt: Securing the Foundations of the Rust Programming Language within the HOPE 2017-track
FTfJP 2017	Author of Iris: A Modular Foundation for Higher-Order Concurrent Separation Logic (KEYNOTE) within the FTfJP 2017-track
ECOOP 2017	Author of Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris within the ECOOP Research Papers-track
PLDI 2017	Author of Repairing Sequential Consistency in C/C++11 within the PLDI Research Papers-track
POPL 2017	Session Chair of Type Systems 3 (part of POPL) Committee Member in Program Committee within the POPL-track Author of A Promising Semantics for Relaxed-Memory Concurrency within the POPL-track
PLMW	Committee Member in Speaker within the PLMW-track Author of How to Give Talks That People Can Follow within the PLMW-track
ICFP 2016	Author of Higher-Order Ghost State within the Research Papers-track Committee Member in External Review Committee within the Research Papers-track
PLMW 2016	Committee Member in Speakers within the PLMW-track Author of How to Write Papers So People Can Read Them within the PLMW-track
POPL 2016	Author of Lightweight Verification of Separate Compilation within the Research Papers-track ERC member in External Reviewing Committee ERC member in External Reviewing Committee within the Research Papers-track
PLMW	Author of How to Write Papers So People Can Read Them within the PLMW-track Committee Member in Organizing Committee
PLDI 2015	Author of Verifying Read-Copy-Update in a Logic for Weak Memory within the Research Papers-track Committee Member in External Review Committee within the Research Papers-track
ESOP 2015	Committee Member in Program Committee within the ESOP-track
SPLASH 2014	Author of GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation within the OOPSLA-track Presenter of GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation within the OOPSLA Artifacts-track