Cătălin Hriţcu
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
- PriSC2 editions2023–2026
- PLDI Workshop Honoring Andreas Podelski2 editions2022–2026
- CPP2 editions2020–2024
all 7 in the filters
on a stage with
all 40 in the filters
who talks about the same things
- Exequiel Rivas6 talks
- Danel Ahman7 talks
- Cédric Fournet7 talks
- Guido Martínez10 talks
- Cezar-Constantin Andrici8 talks
- Théo Winterhalter14 talks
| title | conference | date |
|---|---|---|
| Project Everest: Perspectives from Developing Industrial-Grade High-Assurance(…) | PLDI 2026 | 2026-06-15 |
Project Everest produces a verified TLS stack and crypto suite rather than promises: it yields 1.3 million lines of F source that build in two hours, emits… | ||
| Towards formally secure compilation of verified F* programs against unverified ML(…) | PriSC 2026 | 2026-01-11 |
Framework written and verified in F compiles terminating higher-order IO F programs to a deeply embedded ML-like language with an end-to-end mechanized proof… | ||
| Blame-aware Recomposition for Formally Secure Low-level Compiler Backends | PriSC 2026 | 2026-01-11 |
This work extends recomposition with blame-aware recomposition and an overlay semantics that treats cross-compartment observations (like code-size or… | ||
| FSLH: Flexible Mechanized Speculative Load Hardening | PriSC 2026 | 2026-01-11 |
Presents FSLH, a middle-ground Spectre v1 mitigation that uses a static information‑flow analysis plus selective masking and a semantics that inserts masks (an… | ||
| SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F* | ICFP 2025 | 2025-10-12 |
SecRef is a secure-compilation framework for F that enforces verified programs’ assumptions about dynamically shared ML-style mutable references by inserting… | ||
| My Journey in Secure Compilation | PLMW @ POPL 2025 | 2025-01-19 |
Provides a machine-checked compiler pipeline that enforces compartmentalization and limits undefined behavior to compromised compartments, implemented as… | ||
| The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography | CPP 2024 | 2024-01-15 |
Coq is used to connect Hacspec, Jasmin and SSProve into an automated pipeline that produces: a functional Hacspec spec, an imperative SSProve spec, and… | ||
| Securing Verified IO Programs Against Unverified Code in F* | POPL 2024 | 2024-01-14 |
A verified secure compilation pipeline for F programs that perform IO, called SCIO, compiles verified code to a smaller F target and enforces assumptions at… | ||
| Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ... | PriSC 2023 | 2023-01-21 |
Secure compilation chain for an F subset with IO converts static specs into runtime checks and adds a linking-time reference monitor that blocks forbidden… | ||
| SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M... | PriSC 2023 | 2023-01-21 |
Extension of CompCert implements CompCert with compartments that enforces interfaces, disables cross-compartment inlining/tailcalls, and updates Coq… | ||
| Verifying non-terminating programs with IO in F* | HOPE 2022 | 2022-09-11 |
Defines an F effect that specifies IO for both terminating and potentially non-terminating programs, implements an example echo server and most of a simple web… | ||
| Computing Correctly with Inductive Relations | PLDI 2022 | 2022-06-13 |
Tool automatically derives semi-decision enumerators and checkers from inductive relations in Coq, using Ltac2 meta-programming to emit decision procedures… | ||
| CPP 2020 PC Chairs' Report | CPP 2020 | 2020-01-20 |
Conference receives 72 submissions and accepts 27 papers (37.5%); review uses HotCRP and light double‑blind, with 26 PC members plus 79 external reviewers… | ||
| nothing matches | ||