Cover Image

Practical Deductive Verification of OCaml Programs (Extended Version)

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Pereira, Mário
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)
by: Soares, Tiago Lopes, et al.
Published: (2024)

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
by: Chirica, Ion, et al.
Published: (2025)

Adjoint Natural Deduction (Extended Version)
by: Jang, Junyoung, et al.
Published: (2024)

Model Checking as Program Verification by Abstract Interpretation (Extended Version)
by: Baldan, Paolo, et al.
Published: (2025)

Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation
by: Gros, Charlène, et al.
Published: (2024)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
by: Cheng, Ruotong, et al.
Published: (2025)

Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
by: Şakar, Ömer, et al.
Published: (2026)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
by: Tsukada, Takeshi, et al.
Published: (2025)

AutoDeduct: A Tool for Automated Deductive Verification of C Code
by: Amilon, Jesper, et al.
Published: (2025)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
by: Batz, Kevin, et al.
Published: (2025)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
by: Foster, Simon, et al.
Published: (2024)

VerifyThis 2019: A Program Verification Competition (Extended Report)
by: Dross, Claire, et al.
Published: (2020)

A Deductive Refinement Calculus for Differential-Algebraic Programs
by: Hellwig, Jonathan, et al.
Published: (2026)

Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory [Extended Version]
by: Kettmann, Pascal, et al.
Published: (2026)

Context, Judgement, Deduction
by: Coraglia, Greta, et al.
Published: (2021)

Deductive Systems for Logic Programs with Counting
by: Fandinno, Jorge, et al.
Published: (2025)

HaliVer: Deductive Verification and Scheduling Languages Join Forces
by: Haak, Lars B. van den, et al.
Published: (2024)

Probabilistic Linear Logic Programming with an Application to Bayesian Network Computations (Extended Version)
by: Acclavio, Matteo, et al.
Published: (2026)

Cut-free Deductive System for Continuous Intuitionistic Logic
by: Geoffroy, Guillaume
Published: (2025)

Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics (Extended Version)
by: Kettmann, Pascal, et al.
Published: (2025)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
by: Haselwarter, Philipp G., et al.
Published: (2026)

On the Verification Problem of Remote Direct Memory Access programs (Extended Version with Appendix)
by: Abdulla, Parosh Aziz, et al.
Published: (2026)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
by: Elad, Neta, et al.
Published: (2023)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Splitting Answer Set Programs with respect to Intensionality Statements (Extended Version)
by: Fandinno, Jorge, et al.
Published: (2025)

Craig Interpolation in Program Verification
by: Rümmer, Philipp
Published: (2026)

Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deduction
by: Xu, Yang, et al.
Published: (2025)

Towards Proving Liveness on Weak Memory (Extended Version)
by: Bargmann, Lara, et al.
Published: (2026)

Satisfiability Modulo Extensional Constant Arrays (Extended Version)
by: Preiner, Mathias, et al.
Published: (2026)

Sharing and Linear Logic with Restricted Access (Extended Version)
by: Barenbaum, Pablo, et al.
Published: (2025)

First-Order LTLf Synthesis with Lookback (Extended Version)
by: Winkler, Sarah
Published: (2025)

Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)
by: Acclavio, Matteo, et al.
Published: (2025)

A Hyperlogic for Strategies in Stochastic Games (Extended Version)
by: Gerlach, Lina, et al.
Published: (2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Small Decision Trees for MDPs with Deductive Synthesis
by: Andriushchenko, Roman, et al.
Published: (2025)

Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
by: Gerlach, Lina, et al.
Published: (2025)

Certified Branch-and-Bound MaxSAT Solving (Extended Version)
by: Vandesande, Dieter, et al.
Published: (2025)

Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version)
by: Caires-Santos, Ali K., et al.
Published: (2025)

Partially Finite Model Reasoning in Description Logics Extended Version
by: Gogacz, Tomasz, et al.
Published: (2026)

Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)
by: Paulus, Joseph W. N., et al.
Published: (2021)