Image de couverture de livre

Precise Reasoning About Container-Internal Pointers with Logical Pinning

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Guan, Yawen, Pit-Claudel, Clément
Format:	Preprint
Publié:	2025
Sujets:	Programming Languages D.2.4; F.3.1
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
par: Accattoli, Beniamino, et autres
Publié: (2025)

Bottom-up computation using trees of sublists (Functional Pearl)
par: Mu, Shin-Cheng
Publié: (2023)

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
par: Baier, Daniel, et autres
Publié: (2024)

MoXIchecker: An Extensible Model Checker for MoXI
par: Ates, Salih, et autres
Publié: (2024)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine
par: Gross, Jason, et autres
Publié: (2022)

Verified VCG and Verified Compiler for Dafny
par: Nezamabadi, Daniel, et autres
Publié: (2025)

Seamless, Correct, and Generic Programming over Serialised Data
par: Allais, Guillaume
Publié: (2023)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
par: Frenkel, Eden, et autres
Publié: (2026)

Weak-linearity, globality and in-place update
par: Gramaglia, Hector
Publié: (2024)

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
par: Suwa, Takashi, et autres
Publié: (2026)

Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
par: Beyer, Dirk, et autres
Publié: (2022)

Modelling Distributed Applications with Mixed-Choice Stateful Typestates
par: Parrinha, Francisco, et autres
Publié: (2026)

The pitfalls of verifying floating-point computations
par: Monniaux, David
Publié: (2007)

On the Decidability of Verification under Release/Acquire
par: Conrado, Giovanna Kobus, et autres
Publié: (2026)

A New Interaction Concept for Interactive and Autoactive Program Verification
par: Pfeifer, Wolfram, et autres
Publié: (2026)

Model Checking Probabilistic Operator Precedence Automata
par: Pontiggia, Francesco, et autres
Publié: (2024)

Certified Purity for Cognitive Workflow Executors: From Static Analysis to Cryptographic Attestation
par: McCann, Alan L.
Publié: (2026)

The concept of class invariant in object-oriented programming
par: Meyer, Bertrand, et autres
Publié: (2021)

Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
par: Lahiri, Shuvendu K.
Publié: (2026)

Uniform Substitution for Differential Refinement Logic
par: Prebet, Enguerrand, et autres
Publié: (2024)

Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries
par: McCann, Alan L.
Publié: (2026)

Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
par: McCann, Alan L.
Publié: (2026)

Grounded Language Design for Lightweight Diagramming for Formal Methods
par: Prasad, Siddhartha, et autres
Publié: (2024)

Automatic Function Annotations for Hoare Logic
par: Matichuk, Danielle
Publié: (2012)

Gradual Guarantee via Step-Indexed Logical Relations in Agda
par: Siek, Jeremy G.
Publié: (2024)

Quantitative Verification with Neural Networks
par: Abate, Alessandro, et autres
Publié: (2023)

Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
par: Sundaram, Aarthi, et autres
Publié: (2021)

Policy as Code, Policy as Type
par: Fuchs, Matthew D.
Publié: (2025)

Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
par: Zaiser, Fabian, et autres
Publié: (2024)

Generically Automating Separation Logic by Functors, Homomorphisms and Modules
par: Xu, Qiyuan, et autres
Publié: (2024)

Baking for Dafny: A CakeML Backend for Dafny
par: Nezamabadi, Daniel, et autres
Publié: (2025)

Context-Dependent Effects and Concurrency in Guarded Interaction Trees
par: Stepanenko, Sergei, et autres
Publié: (2025)

Uniqueness is Separation
par: O'Connor, Liam, et autres
Publié: (2026)

Space-time process algebra with asynchronous communication
par: Bergstra, J. A., et autres
Publié: (2024)

Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
par: Lin, Hongyu, et autres
Publié: (2026)

Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence
par: McCann, Alan L.
Publié: (2026)

Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
par: Amusuo, Paschal C., et autres
Publié: (2025)

QuickCheck for VDM
par: Battle, Nick, et autres
Publié: (2024)

A Unit Proofing Framework for Code-level Verification: A Research Agenda
par: Amusuo, Paschal C., et autres
Publié: (2024)

A Gentle Overview of Asynchronous Session-based Concurrency: Deadlock Freedom by Typing
par: Heuvel, Bas van den, et autres
Publié: (2024)