Cover Image

Verified VCG and Verified Compiler for Dafny

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Nezamabadi, Daniel, Myreen, Magnus O., Tan, Yong Kiam
Format:	Preprint
Published:	2025
Subjects:	Programming Languages Logic in Computer Science D.2.4; D.3.1; D.3.4; F.3.1; F.3.2
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Baking for Dafny: A CakeML Backend for Dafny
by: Nezamabadi, Daniel, et al.
Published: (2025)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine
by: Gross, Jason, et al.
Published: (2022)

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
by: Suwa, Takashi, et al.
Published: (2026)

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

The Denotational Semantics of SSA
by: Ghalayini, Jad Elkhaleq, et al.
Published: (2024)

TensorRight: Automated Verification of Tensor Graph Rewrites
by: Arora, Jai, et al.
Published: (2025)

Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations
by: Knothe, David, et al.
Published: (2026)

Modelling Distributed Applications with Mixed-Choice Stateful Typestates
by: Parrinha, Francisco, et al.
Published: (2026)

Verification of E-Voting Algorithms in Dafny
by: Büttner, Robert, et al.
Published: (2025)

Explicit Weakening
by: Wadler, Philip
Published: (2024)

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
by: Baier, Daniel, et al.
Published: (2024)

MoXIchecker: An Extensible Model Checker for MoXI
by: Ates, Salih, et al.
Published: (2024)

Gradual Guarantee via Step-Indexed Logical Relations in Agda
by: Siek, Jeremy G.
Published: (2024)

Genericity Through Stratification
by: Arrial, Victor, et al.
Published: (2024)

AdapTT: Functoriality for Dependent Type Casts
by: Adjedj, Arthur, et al.
Published: (2025)

Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
by: Zaiser, Fabian, et al.
Published: (2024)

Definitional Functoriality for Dependent (Sub)Types -- Extended version
by: Laurent, Théo, et al.
Published: (2023)

Weak-linearity, globality and in-place update
by: Gramaglia, Hector
Published: (2024)

What does it take to certify a conversion checker?
by: Lennon-Bertrand, Meven
Published: (2025)

Separation Logic of Generic Resources via Sheafeology
by: van Starkenburg, Berend, et al.
Published: (2025)

Unified Fairness for Weak Memory Verification
by: Abdulla, Parosh Aziz, et al.
Published: (2023)

A New Interaction Concept for Interactive and Autoactive Program Verification
by: Pfeifer, Wolfram, et al.
Published: (2026)

Teaching Introductory Functional Programming Using Haskelite
by: Vasconcelos, Pedro
Published: (2025)

Complementing an imperative process algebra with a rely/guarantee logic
by: Middelburg, C. A.
Published: (2025)

Probabilistic imperative process algebra
by: Middelburg, C. A.
Published: (2026)

Bottom-up computation using trees of sublists (Functional Pearl)
by: Mu, Shin-Cheng
Published: (2023)

Precise Reasoning About Container-Internal Pointers with Logical Pinning
by: Guan, Yawen, et al.
Published: (2025)

A Graded Modal Type Theory for Pulse Schedules
by: Adams, Robin, et al.
Published: (2025)

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

Model Checking Probabilistic Operator Precedence Automata
by: Pontiggia, Francesco, et al.
Published: (2024)

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

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

On Modular Termination Proofs of General Logic Programs
by: Bossi, Annalisa, et al.
Published: (2000)

Sequence-Based Abstract Interpretation of Prolog
by: Charlier, Baudouin Le, et al.
Published: (2000)

Grounded Language Design for Lightweight Diagramming for Formal Methods
by: Prasad, Siddhartha, et al.
Published: (2024)

Constrained LTL Specification Learning from Examples
by: Zhang, Changjian, et al.
Published: (2024)

Quantitative Assurance and Synthesis of Controllers from Activity Diagrams
by: Ye, Kangfeng, et al.
Published: (2024)

Policy as Code, Policy as Type
by: Fuchs, Matthew D.
Published: (2025)

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)
by: Sextl, Florian, et al.
Published: (2023)

SMT-based Symbolic Model-Checking for Operator Precedence Languages
by: Chiari, Michele, et al.
Published: (2024)