Imagen de Portada

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

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Gros, Charlène, Pereira, Mário
Formato:	Preprint
Publicado:	2024
Materias:	Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Regular Typed Unification
por: Barbosa, João, et al.
Publicado: (2024)

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

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

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

Demystifying $μ$
por: Afshari, Bahareh, et al.
Publicado: (2024)

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

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

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

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

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

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

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

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

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

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

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

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

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