Cover Image

(Dis)Proving Spectre Security with Speculation-Passing Style

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Arranz-Olmos, Santiago, Barthe, Gilles, Blatter, Lionel, Xie, Xingyu, Zhang, Zhiyuan
Format:	Preprint
Published:	2025
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

The Jasmin Compiler Preserves Cryptographic Security
by: Arranz-Olmos, Santiago, et al.
Published: (2025)

Decompiling for Constant-Time Analysis
by: Arranz-Olmos, Santiago, et al.
Published: (2025)

D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
by: Xu, Yingte, et al.
Published: (2025)

Laws of Quantum Programming
by: Ying, Mingsheng, et al.
Published: (2024)

Automating Equational Proofs in Dirac Notation
by: Xu, Yingte, et al.
Published: (2024)

Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
by: Fabian, Xaver, et al.
Published: (2024)

Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
by: Lundén, Daniel, et al.
Published: (2023)

TypeDis: A Type System for Disentanglement
by: Moine, Alexandre, et al.
Published: (2025)

Traq: Estimating the Quantum Cost of Classical Programs
by: Peduri, Anurudh, et al.
Published: (2025)

Automated Discovery of Tactic Libraries for Interactive Theorem Proving
by: Xin, Yutong, et al.
Published: (2025)

Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
by: Zhao, Jianhong, et al.
Published: (2025)

Proving Functional Program Equivalence via Directed Lemma Synthesis
by: Sun, Yican, et al.
Published: (2024)

A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
by: Xu, Qiyuan, et al.
Published: (2025)

A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs
by: Amtoft, Torben, et al.
Published: (2024)

Proving Confluence in the Confluence Framework with CONFident
by: Gutiérrez, Raúl, et al.
Published: (2023)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

DisQ: A Model of Distributed Quantum Processors (Extended Version)
by: Chang, Le, et al.
Published: (2024)

A Language-Agnostic Logical Relation for Message-Passing Protocols
by: Zhang, Tesla, et al.
Published: (2025)

Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
by: Zhang, Tesla, et al.
Published: (2025)

Actegories, Copowers, and Higher-Order Message Passing Semantics
by: Cockett, Robin, et al.
Published: (2025)

The Long Way to Deforestation (Technical Report): A Type Inference and Elaboration Technique for Removing Intermediate Data Structures
by: Chen, Yijia, et al.
Published: (2024)

Beyond Pass-by-Pass Optimization: Intent-Driven IR Optimization with Large Language Models
by: Qiu, Lei, et al.
Published: (2026)

A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics
by: Barthe, Gilles, et al.
Published: (2025)

FSLH: Flexible Mechanized Speculative Load Hardening
by: Baumann, Jonathan, et al.
Published: (2025)

Agentic Proving for Program Verification
by: Sosso, Alessandro, et al.
Published: (2026)

Non-Termination Proving: 100 Million LoC and Beyond
by: Vanegue, Julien, et al.
Published: (2025)

Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings
by: Bagrel, Thomas
Published: (2026)

Semantic Logical Relations for Timed Message-Passing Protocols (Extended Version)
by: Yao, Yue, et al.
Published: (2024)

An Asynchronous Scheme for Rollback Recovery in Message-Passing Concurrent Programming Languages
by: Vidal, Germán
Published: (2023)

Refinements for Multiparty Message-Passing Protocols: Specification-agnostic theory and implementation
by: Martin, Vassor, et al.
Published: (2024)

PassNet: Scaling Large Language Models for Graph Compiler Pass Generation
by: Liu, Yiqun, et al.
Published: (2026)

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
by: Carreira, Carolina, et al.
Published: (2025)

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
by: Fedchin, Aleksandr, et al.
Published: (2025)

SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
by: van der Wall, Sören, et al.
Published: (2024)

Multi-Pass Targeted Dynamic Symbolic Execution
by: Yavuz, Tuba
Published: (2024)

A Direct-Style Effect Notation for Sequential and Parallel Programs
by: Richter, David, et al.
Published: (2023)

Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
by: Matsushita, Yusuke, et al.
Published: (2026)

Filament: Denning-Style Information Flow Control for Rust
by: Ching, Jeffrey C., et al.
Published: (2026)

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
by: Baumann, Jonathan, et al.
Published: (2026)

EAGLE-Pangu: Accelerator-Safe Tree Speculative Decoding on Ascend NPUs
by: Han, Chang, et al.
Published: (2026)