Imagen de Portada

Mechanised Hypersafety Proofs about Structured Data: Extended Version

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Gladshtein, Vladimir, Zhao, Qiyuan, Ahrens, Willow, Amarasinghe, Saman, Sergey, Ilya
Formato:	Preprint
Publicado:	2024
Materias:	Programming Languages Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Small Scale Reflection for the Working Lean User
por: Gladshtein, Vladimir, et al.
Publicado: (2024)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
por: Cheng, Ruotong, et al.
Publicado: (2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
por: Li, Kwing Hei, et al.
Publicado: (2025)

Adjoint Natural Deduction (Extended Version)
por: Jang, Junyoung, et al.
Publicado: (2024)

Ordered Adjoint Logic (Extended Version)
por: Roshal, Sophia, et al.
Publicado: (2026)

Hybrid Intersection Types for PCF (Extended Version)
por: Barenbaum, Pablo, et al.
Publicado: (2024)

An Abstract Domain for Heap Commutativity (Extended Version)
por: Pincus, Jared, et al.
Publicado: (2024)

Monadic Intersection Types, Relationally (Extended Version)
por: Gavazzo, Francesco, et al.
Publicado: (2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
por: Lööw, Andreas, et al.
Publicado: (2024)

An Introduction to Different Approaches to Initial Semantics
por: Lamiaux, Thomas, et al.
Publicado: (2024)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
por: Li, Kwing Hei, et al.
Publicado: (2025)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
por: Tsukada, Takeshi, et al.
Publicado: (2025)

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
por: Lahav, Ori, et al.
Publicado: (2023)

JAX Autodiff from a Linear Logic Perspective (Extended Version)
por: Giusti, Giulia, et al.
Publicado: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
por: Grandury, Marcos, et al.
Publicado: (2025)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
por: Haselwarter, Philipp G., et al.
Publicado: (2026)

A Unified Framework for Initial Semantics
por: Lamiaux, Thomas, et al.
Publicado: (2025)

Symmetric Proofs of Parameterized Programs
por: Cheng, Ruotong, et al.
Publicado: (2026)

Coinductive Proofs for Temporal Hyperliveness
por: Correnson, Arthur, et al.
Publicado: (2025)

Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
por: Deng, Haotian, et al.
Publicado: (2025)

Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
por: Voichick, Finn, et al.
Publicado: (2022)

More Church-Rosser Proofs in BELUGA
por: Momigliano, Alberto, et al.
Publicado: (2024)

To bind or not to bind? Discovering Stable Relationships in Object-centric Processes (Extended Version)
por: Seidel, Anjo, et al.
Publicado: (2025)

Cyclic Proofs in Hoare Logic and its Reverse
por: Brotherston, James, et al.
Publicado: (2025)

Pleasant Imperative Program Proofs with GallinaC
por: Fort, Frédéric, et al.
Publicado: (2025)

Handling the Selection Monad (Full Version)
por: Plotkin, Gordon, et al.
Publicado: (2025)

Linearization via Rewriting (Long Version)
por: Lago, Ugo Dal, et al.
Publicado: (2025)

Zippy -- Generic White-Box Proof Search with Zippers
por: Kappelmann, Kevin
Publicado: (2025)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
por: Vollmer, Victoria, et al.
Publicado: (2024)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
por: Oda, Yukihiro
Publicado: (2025)

Insum: Sparse GPU Kernels Simplified and Optimized with Indirect Einsums
por: Won, Jaeyeon, et al.
Publicado: (2025)

Functional Array Programming in an Extended Pi-Calculus
por: Hüttel, Hans, et al.
Publicado: (2024)

Extended Abstract: Mutable Objects with Several Implementations
por: Kaufmann, Matt, et al.
Publicado: (2025)

Automated Verification of Monotonic Data Structure Traversals in C
por: Sotoudeh, Matthew
Publicado: (2025)

Logical Relations for Formally Verified Authenticated Data Structures
por: Gregersen, Simon Oddershede, et al.
Publicado: (2025)

Reasoning about Weak Isolation Levels in Separation Logic
por: Mathiasen, Anders Alnor, et al.
Publicado: (2025)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
por: Elad, Neta, et al.
Publicado: (2025)

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
por: Poli, Federico, et al.
Publicado: (2024)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
por: Stübinger, Terru, et al.
Publicado: (2023)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
por: Aguirre, Alejandro, et al.
Publicado: (2024)