conf.researchr.org / Derek Dreyer
Registered user since Sun 28 Sep 2014
Contributions
2024
PLDI
RTFM
- Moderator of Panel: Promotion and Tenure within the RTFM 2024: Red-Hot Topics in Faculty Mentoring-track
- Session Chair of Session 2 (part of RTFM 2024: Red-Hot Topics in Faculty Mentoring)
- Organizer of Opening within the RTFM 2024: Red-Hot Topics in Faculty Mentoring-track
- Committee Member in Organizing Committee within the RTFM 2024: Red-Hot Topics in Faculty Mentoring-track
POPL
PLMW
2023
SPLASH
- Author of Stuttering for Free within the OOPSLA-track
- Author of Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning within the OOPSLA-track
- Author of Melocoton: A Program Logic for Verified Interoperability Between OCaml and C within the OOPSLA-track
- Associate Chair in OOPSLA Review Committee within the OOPSLA-track
2022
SPLASH
- 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
PLDI
- 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
2021
ICFP
PLDI
2020
PLMW
POPL
- 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
2019
SPLASH
PLMW
ICFP
2018
SPLASH
ICFP
- 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
POPL
- 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