Image de couverture de livre

Incremental Proof Development in Dafny with Module-Based Induction

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Ho, Son, Pit-Claudel, Clément
Format:	Preprint
Publié:	2024
Sujets:	Programming Languages
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Automatic layout of railroad diagrams
par: Chiplunkar, Shardul, et autres
Publié: (2025)

Linear Matching of JavaScript Regular Expressions
par: Barrière, Aurèle, et autres
Publié: (2023)

Tracers for debugging and program exploration
par: Chiplunkar, Shardul, et autres
Publié: (2026)

Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
par: Barrière, Aurèle, et autres
Publié: (2025)

On the computational complexity of JavaScript regex matching
par: Deng, Victor, et autres
Publié: (2026)

Precise Reasoning About Container-Internal Pointers with Logical Pinning
par: Guan, Yawen, et autres
Publié: (2025)

A Coq Mechanization of JavaScript Regular Expression Semantics
par: De Santo, Noé, et autres
Publié: (2024)

Source-to-Source Transformations for GPU Code Generation
par: de Castelnau, Julien, et autres
Publié: (2026)

Verified and Optimized Implementation of Orthologic Proof Search
par: Guilloud, Simon, et autres
Publié: (2025)

MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
par: Amaral, Isabel, et autres
Publié: (2025)

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
par: Fedchin, Aleksandr, et autres
Publié: (2025)

Leveraging Large Language Models to Boost Dafny's Developers Productivity
par: Silva, Álvaro, et autres
Publié: (2024)

Towards AI-Assisted Synthesis of Verified Dafny Methods
par: Misu, Md Rakib Hossain, et autres
Publié: (2024)

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

Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
par: Wu, Valentina, et autres
Publié: (2025)

dafny-annotator: AI-Assisted Verification of Dafny Programs
par: Poesia, Gabriel, et autres
Publié: (2024)

Dafny as Verification-Aware Intermediate Language for Code Generation
par: Li, Yue Chen, et autres
Publié: (2025)

Inferring multiple helper Dafny assertions with LLMs
par: Silva, Álvaro, et autres
Publié: (2025)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
par: Ukhanov, Evgeny
Publié: (2025)

DafnyBench: A Benchmark for Formal Software Verification
par: Loughridge, Chloe, et autres
Publié: (2024)

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
par: Carreira, Carolina, et autres
Publié: (2025)

Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)
par: Ho, Son, et autres
Publié: (2024)

Scenario-Based Proofs for Concurrent Objects [Extended Version]
par: Enea, Constantin, et autres
Publié: (2023)

Guided Sketch-Based Program Induction by Search Gradients
par: Amin, Ahmad Ayaz
Publié: (2024)

Incremental units-of-measure verification
par: Danish, Matthew, et autres
Publié: (2024)

Incremental Computation: What Is the Essence?
par: Liu, Yanhong A.
Publié: (2023)

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)
par: Schüssele, Frank, et autres
Publié: (2025)

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

Incremental Live Programming via Shortcut Memoization
par: Kirisame, Marisa, et autres
Publié: (2026)

Incremental Bidirectional Typing via Order Maintenance
par: Porter, Thomas J., et autres
Publié: (2025)

Charon: An Analysis Framework for Rust
par: Ho, Son, et autres
Publié: (2024)

A Natural Formalized Proof Language
par: Xie, Lihan, et autres
Publié: (2024)

Automating Equational Proofs in Dirac Notation
par: Xu, Yingte, et autres
Publié: (2024)

Proof Repair across Quotient Type Equivalences
par: Viola, Cosmo, et autres
Publié: (2023)

Adaptive Shielding via Parametric Safety Proofs
par: Feng, Yao, et autres
Publié: (2025)

Agentic Proof Automation: A Case Study
par: Xu, Yichen, et autres
Publié: (2026)

Asynchronous Global Protocols, Precisely: Full Proofs
par: Pischke, Kai, et autres
Publié: (2025)

Tail Modulo Cons, OCaml, and Relational Separation Logic
par: Allain, Clément, et autres
Publié: (2024)

FlowLog: Efficient and Extensible Datalog via Incrementality
par: Zhao, Hangdong, et autres
Publié: (2025)

An Incremental Algorithm for Algebraic Program Analysis
par: Zhou, Chenyu, et autres
Publié: (2024)