Cover Image

Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Gros, Charlène, 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

Practical Deductive Verification of OCaml Programs (Extended Version)
by: Pereira, Mário
Published: (2024)

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)

Towards benchmarking of Solidity verification tools
by: Bartoletti, Massimo, et al.
Published: (2024)

On verification and constraint generation for families of similar hybrid automata
by: Sofronie-Stokkermans, Viorica, et al.
Published: (2025)

Operational semantics and program verification using many-sorted hybrid modal logic
by: Leustean, Ioana, et al.
Published: (2019)

Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
by: Cimatti, Alessandro, et al.
Published: (2024)

OSVAuto: automatic proofs about functional specifications in OS verification
by: Wu, Yulun, et al.
Published: (2024)

On the logical structure of choice and bar induction principles
by: Brede, Nuria, et al.
Published: (2021)

Vers une modélisation de la confiance dans le renseignement sur les menaces cyber
by: Bobelin, Laurent, et al.
Published: (2025)

A logic for default deontic reasoning
by: Piazza, Mario, et al.
Published: (2025)

Contractions of quasi relation algebras and applications to representability
by: Craig, Andrew, et al.
Published: (2026)

On describing trees and quasi-trees from their leaves
by: Courcelle, Bruno
Published: (2025)

A SAT-based approach to rigorous verification of Bayesian networks
by: Stępka, Ignacy, et al.
Published: (2024)

Why does it fail? Explanation of verification failures
by: Eriksson, Lars-Henrik
Published: (2026)

StepProof: Step-by-step verification of natural language mathematical proofs
by: Hu, Xiaolin, et al.
Published: (2025)

KindHML: formal verification of smart contracts based on Hennessy-Milner logic
by: Bartoletti, Massimo, et al.
Published: (2026)

Duality theory and representations for distributive quasi relation algebras and DInFL-algebras
by: Craig, Andrew, et al.
Published: (2025)

Refutation calculi for lattice-based logics: from display to tableaux
by: De Domenico, Andrea, et al.
Published: (2026)

A beginner guide to Iris, Coq and separation logic
by: Dietrich, Elizabeth
Published: (2021)

Sequent Calculi for Data-Aware Modal Logics
by: Areces, Carlos, et al.
Published: (2025)

An ecumenical view of proof-theoretic semantics
by: Nascimento, Victor, et al.
Published: (2023)

Regular Typed Unification
by: Barbosa, João, et al.
Published: (2024)

Comparing and Contrasting Arrow's Impossibility Theorem and Gödel's Incompleteness Theorem
by: Livson, Ori, et al.
Published: (2025)

A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics
by: Oda, Yukihiro
Published: (2025)

Abstract computation over first-order structures. Part IIa: Moschovakis' operator and other non-determinisms
by: Gaßner, Christine
Published: (2025)

Demystifying $μ$
by: Afshari, Bahareh, et al.
Published: (2024)

Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions
by: Artale, Alessandro, et al.
Published: (2025)

Proof-theoretic Semantics for Second-order Logic
by: Gheorghiu, Alexander V., et al.
Published: (2025)

List types for resource aware languages: an implicit name approach
by: Ghilezan, Silvia, et al.
Published: (2021)

Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
by: Afshari, Bahareh, et al.
Published: (2024)

Many-valued coalgebraic dynamic logics: Safety and strong completeness via reducibility
by: Hansen, Helle Hvid, et al.
Published: (2025)

Generalized Decidability via Brouwer Trees
by: de Jong, Tom, et al.
Published: (2026)

Constructive higher sheaf models with applications to synthetic mathematics
by: Coquand, Thierry, et al.
Published: (2026)

Bijective proofs for Eulerian numbers of types B and D
by: Santocanale, Luigi
Published: (2021)

On the logical structure of some maximality and well-foundedness principles equivalent to choice principles
by: Herbelin, Hugo
Published: (2024)

Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
by: Powell, Thomas
Published: (2023)

The strength of the dominance rule
by: Kołodziejczyk, Leszek Aleksander, et al.
Published: (2024)

Dynamic Probability Logic: Decidability & Computability
by: Chopoghloo, Somayeh, et al.
Published: (2024)

A Coalgebraic Semantics for Intuitionistic Modal Logic
by: Almeida, Rodrigo Nicolau, et al.
Published: (2024)