Toggle navigation
Sign in
Sign up
conf.researchr.org
/
Derek Dreyer
conf.researchr.org general profile
ECOOP 2019 profile
ECOOP 2022 profile
ESOP 2015 profile
ICFP 2016 profile
ICFP 2017 profile
ICFP 2018 profile
ICFP 2019 profile
ICFP 2020 profile
ICFP 2021 profile
ICFP 2022 profile
PLDI 2015 profile
PLDI 2020 profile
PLDI 2021 profile
PLDI 2022 profile
PLDI, ECOOP, Curry On, DEBS, LCTES and ISMM profile
POPL 2016 profile
POPL 2017 profile
POPL 2018 profile
POPL 2020 profile
POPL 2021 profile
POPL 2022 profile
POPL 2023 profile
POPL 2024 profile
SPLASH 2014 profile
SPLASH 2017 profile
SPLASH 2018 profile
SPLASH 2019 profile
SPLASH 2022 profile
SPLASH 2023 profile
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
Share
x
Thu 30 Mar 07:18