Cover Image

Adaptive Shielding via Parametric Safety Proofs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Feng, Yao, Zhu, Jun, Platzer, André, Laurent, Jonathan
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

Oracular Programming: A Modular Foundation for Building LLM-Enabled Software
by: Laurent, Jonathan, et al.
Published: (2025)

Hybrid Game Control Envelope Synthesis
by: Kabra, Aditi, et al.
Published: (2025)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
by: Teuber, Samuel, et al.
Published: (2025)

ExVerus: Verus Proof Repair via Counterexample Reasoning
by: Yang, Jun, et al.
Published: (2026)

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

Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types
by: He, Siyuan, et al.
Published: (2026)

A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
by: Bayazıt, Barış, et al.
Published: (2025)

Parametricity via Cohesion
by: Aberlé, C. B.
Published: (2024)

Language-Parametric Reference Synthesis (Extended)
by: Pelsmaeker, Daniel A. A., et al.
Published: (2025)

A Natural Formalized Proof Language
by: Xie, Lihan, et al.
Published: (2024)

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

Asynchronous Global Protocols, Precisely: Full Proofs
by: Pischke, Kai, et al.
Published: (2025)

Proof Repair across Quotient Type Equivalences
by: Viola, Cosmo, et al.
Published: (2023)

Agentic Proof Automation: A Case Study
by: Xu, Yichen, et al.
Published: (2026)

Scenario-Based Proofs for Concurrent Objects [Extended Version]
by: Enea, Constantin, et al.
Published: (2023)

Incremental Proof Development in Dafny with Module-Based Induction
by: Ho, Son, et al.
Published: (2024)

Substructural Parametricity
by: Aberlé, C. B., et al.
Published: (2025)

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
by: Kent, Zachary, et al.
Published: (2025)

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
by: Conoly, Owen, et al.
Published: (2025)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
by: Frenkel, Eden, et al.
Published: (2026)

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)
by: Schüssele, Frank, et al.
Published: (2025)

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

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
by: Paraskevopoulou, Zoe
Published: (2026)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
by: Nagy, Shaan, et al.
Published: (2024)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
by: Ravi, Nikil, et al.
Published: (2026)

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
by: Gross, Jason, et al.
Published: (2023)

Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)
by: Ho, Son, et al.
Published: (2024)

Refactoring and Equivalence in Rust: Expanding the REM Toolchain with a Novel Approach to Automated Equivalence Proofs
by: Britton, Matthew, et al.
Published: (2026)

Coinductive Proofs for Temporal Hyperliveness
by: Correnson, Arthur, et al.
Published: (2025)

Symmetric Proofs of Parameterized Programs
by: Cheng, Ruotong, et al.
Published: (2026)

Unlocking the Power of Environment Assumptions for Unit Proofs
by: Priya, Siddharth, et al.
Published: (2024)

SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation
by: Nezhad, Sina Bagheri, et al.
Published: (2025)

ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
by: Gu, Alex, et al.
Published: (2025)

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

Annotating and Auditing the Safety Properties of Unsafe Rust
by: Rao, Zihao, et al.
Published: (2025)

The CoCompiler: DSL Lifting via Relational Compilation
by: Spargo, Naomi, et al.
Published: (2025)

Parametrizing Reads-From Equivalence for Predictive Monitoring
by: Farzan, Azadeh, et al.
Published: (2026)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
by: Cao, Jialun, et al.
Published: (2025)

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

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