Cover Image

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Fedchin, Aleksandr, Mejr, Antero, Sundar, Hari, Foster, Jeffrey S.
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

MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
by: Amaral, Isabel, et al.
Published: (2025)

Towards AI-Assisted Synthesis of Verified Dafny Methods
by: Misu, Md Rakib Hossain, et al.
Published: (2024)

Verified VCG and Verified Compiler for Dafny
by: Nezamabadi, Daniel, et al.
Published: (2025)

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

dafny-annotator: AI-Assisted Verification of Dafny Programs
by: Poesia, Gabriel, et al.
Published: (2024)

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

Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
by: Wu, Valentina, et al.
Published: (2025)

Dafny as Verification-Aware Intermediate Language for Code Generation
by: Li, Yue Chen, et al.
Published: (2025)

Inferring multiple helper Dafny assertions with LLMs
by: Silva, Álvaro, et al.
Published: (2025)

DafnyBench: A Benchmark for Formal Software Verification
by: Loughridge, Chloe, et al.
Published: (2024)

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

Leveraging Large Language Models to Boost Dafny's Developers Productivity
by: Silva, Álvaro, et al.
Published: (2024)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

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

DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
by: Banerjee, Debangshu, et al.
Published: (2026)

The Complexity of Testing Message-Passing Concurrency
by: Shi, Zheng, et al.
Published: (2025)

Dependent Session Types for Verified Concurrent Programming
by: Fu, Qiancheng, et al.
Published: (2025)

Verifying the Fisher-Yates Shuffle Algorithm in Dafny
by: Zetzsche, Stefan, et al.
Published: (2025)

How to Verify a Turing Machine with Dafny
by: Lederer, Edgar F. A.
Published: (2026)

Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
by: Zetzsche, Stefan, et al.
Published: (2024)

Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation
by: Yang, Xiaoxiao, et al.
Published: (2017)

A Language-Agnostic Logical Relation for 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)

Mason: Type- and Name-Guided Program Synthesis
by: Geer, Jasper, et al.
Published: (2026)

Reduction for Structured Concurrent Programs
by: Gangamreddypalli, Namratha, et al.
Published: (2026)

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

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

Toward Verified Library-Level Choreographic Programming with Algebraic Effects
by: Shen, Gan, et al.
Published: (2024)

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

Caesar: A Deductive Verifier for Probabilistic Programs
by: Schröer, Philipp, et al.
Published: (2026)

Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
by: Yan, Chuanhao, et al.
Published: (2025)

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

The Design of an Interactive Proof Mode for Dafny
by: Ciobâcă, Ştefan, et al.
Published: (2025)

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
by: Reitz, Antonin, et al.
Published: (2024)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
by: Wu, Jinhua, et al.
Published: (2025)

AcrosticSleuth: Probabilistic Identification and Ranking of Acrostics in Multilingual Corpora
by: Fedchin, Aleksandr, et al.
Published: (2024)

KATch: A Fast Symbolic Verifier for NetKAT
by: Moeller, Mark, et al.
Published: (2024)

Qafny: A Quantum-Program Verifier
by: Li, Liyi, et al.
Published: (2022)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

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