Cover Image

Formal Verification of Imperative First-Class Functions in Move

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Grieskamp, Wolfgang, Zhang, Teng, Kashyap, Vineeth, Silverman, Jake
Format:	Preprint
Published:	2026
Subjects:	Programming Languages Logic in Computer Science Software Engineering 68Q60 D.2.4; F.3.1; D.3.3
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Combining Mechanical and Agentic Specification Inference for Move
by: Grieskamp, Wolfgang, et al.
Published: (2026)

Monitoring Hyperproperties over Observed and Constructed Traces
by: Chalupa, Marek, et al.
Published: (2025)

Array-Carrying Symbolic Execution for Function Contract Generation
by: Lu, Weijie, et al.
Published: (2026)

Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers
by: Zhang, Manqing, et al.
Published: (2026)

Contract-based Verification of Digital Twins
by: Naeem, Muhammad, et al.
Published: (2025)

The concept of class invariant in object-oriented programming
by: Meyer, Bertrand, et al.
Published: (2021)

Multiple Query Satisfiability of Constrained Horn Clauses
by: De Angelis, Emanuele, et al.
Published: (2022)

Transport via Partial Galois Connections and Equivalences
by: Kappelmann, Kevin
Published: (2023)

Verification of Quantum Protocols Adopting Physically Admissible Schedulers
by: Ceragioli, Lorenzo, et al.
Published: (2026)

On systematic construction of correct logic programs
by: Drabent, Włodzimierz
Published: (2025)

Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation
by: Alpay, Faruk, et al.
Published: (2025)

Tridirectional Discriminating-Power Formal Verification of Smart Contract Reentrancy Defense Against Production-Deployed Solidity Source
by: Iskander, Ray
Published: (2026)

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

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

Decidable Reversible Equivalences for Finite Petri Nets
by: Gorrieri, Roberto, et al.
Published: (2025)

Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
by: Reinhard, Tobias
Published: (2024)

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

Bounded Modal Logic
by: Murase, Yuito, et al.
Published: (2026)

Simple Types for Polymorphic Functions
by: Jay, Barry, et al.
Published: (2026)

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

Quantifying Confidence in Assurance 2.0 Arguments
by: Bloomfield, Robin, et al.
Published: (2026)

Principal Types as Partial Involutions
by: Honsell, Furio, et al.
Published: (2024)

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

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

A Unit Proofing Framework for Code-level Verification: A Research Agenda
by: Amusuo, Paschal C., et al.
Published: (2024)

Collatz conjecture becomes theorem
by: Mirkowska, Grażyna, et al.
Published: (2023)

Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
by: Amusuo, Paschal C., et al.
Published: (2025)

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

Automatic Function Annotations for Hoare Logic
by: Matichuk, Danielle
Published: (2012)

Nominal techniques as an Agda library
by: Gabbay, Murdoch J., et al.
Published: (2026)

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

Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
by: Lin, Hongyu, et al.
Published: (2026)

Simulating and model checking membrane systems using strategies in Maude
by: Rubio, Rubén, et al.
Published: (2024)

Quantum Bisimilarity is a Congruence under Physically Admissible Schedulers
by: Ceragioli, Lorenzo, et al.
Published: (2024)

Totality for Mixed Inductive and Coinductive Types
by: Hyvernat, Pierre
Published: (2019)

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

CETBench: A Novel Dataset constructed via Transformations over Programs for Benchmarking LLMs for Code-Equivalence Checking
by: Oza, Neeva, et al.
Published: (2025)

Strategies, model checking and branching-time properties in Maude
by: Rubio, Rubén, et al.
Published: (2024)

Model checking strategy-controlled systems in rewriting logic
by: Rubio, Rubén, et al.
Published: (2024)

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