back to home page
Cătălin Hrițcu
Talks
Here you find materials from most of the talks I have given so far.
- Journey Beyond Full Abstraction:
Exploring Robust Property Preservation for Secure Compilation
- Verified Effectful Programming in F*
- When Good Components Go Bad
- Formally Secure Compilation
- What is secure compilation?
- Principles of Secure Compilation, PriSC'18
- Program Chair's Welcome Message: slides (2018-01-13)
- What's new in F*?
- Presentation of Inria Prosecco team
- European Symposium on Security and Privacy, EuroS&P 2017
- General Chair's Welcome Message: slides (2017-04-26)
- Efficient Formally Secure Compilers to a Tagged Architecture
- What is secure compilation?
- Dependent Types and Multi-Monadic Effects in F*
- More Secure Software Systems by
Formal Verification,
Property-Based Testing, Secure
Compilation, and Dynamic Monitoring
- Invited Vision Talk at Scientific Committee meeting of
Nokia's Bell Labs
-- Inria common lab:
slides
(2015-12-15)
- Micro-Policies: Formally Verified, Tag-Based Security Monitors
- Foundational Property-Based Testing
- QuickChick: Property-based testing for Coq
- Testing Noninterference, Quickly
- Formally Verified Privacy-Preserving Distributed Applications
- All Your IFCException Are Belong To Us
- CRASH/SAFE: Clean-slate Co-design of a Secure Host Architecture
- Poison-pills and dynamic information flow control
- On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols
- Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis
- Thesis defense, Saarland University: slides (2012-01-10)
- Breeze: A Language For Writing Secure Software
- Union, Intersection, and Refinement Types and Reasoning about Type Disjointness for Analyzing Protocol Implementations
- Semantic Subtyping with an SMT Solver
- Type-checking Implementations of Protocols Based on Zero-knowledge Proofs - Work in Progress
- Achieving Security Despite Compromise Using Zero-knowledge
- Type-checking Zero-knowledge
- Automatic Verification of Remote Electronic Voting Protocols
- Evidence-based Audit (presented only)
- Refinement Types for Secure Implementations (presented only)
- Improving Security Despite Compromise with Zero-knowledge
- A Type Discipline for Authorization in Distributed Systems (presented only)
- Demand-Driven Alias Analysis for C (presented only)
- Step-indexed Semantics of Imperative Objects
- Verifying Security Protocols and their Implementations (presented only)
- Low-Level Software Security: Attacks and Defenses; Control Flow Integrity (presented only)
- Step-indexed Semantic Model of Types for the Functional Object Calculus
- Programming System Lab: slides (2007-06-21)
- Step-indexed Semantics of Imperative Objects (abstract)
- Mining Version Archives (presented only)
- Empirical Software Engineering Seminar (SS 2006): slides, notes (2006-07-08)
- FluXQuery: An Optimizing XQuery Processor for Streaming XML Data (presented only)
- A Reference Implementation of ADF: Semantic Web-based Agent Communication
- SYNASC - Workshop on Agents for Complex Systems, ACSys 2005: slides (2005-09-25)
- Designing a Multiprecision Number Theory Library
- NATO Advanced Research Workshop on Concurrent Information Processing and Computing: slides (2003-07-10)