Imagen de Portada

Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Ciccalè, Marco, Jurjo-Rivas, Daniel, Morales, Jose F., López-García, Pedro, Hermenegildo, Manuel V.
Formato:	Preprint
Publicado:	2025
Materias:	Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Exploiting Multiple Abstract Call Patterns for Optimizing Run-Time Checks
por: Ferreiro, Daniela, et al.
Publicado: (2026)

Abstract Environment Trimming
por: Jurjo-Rivas, Daniel, et al.
Publicado: (2024)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
por: Rustenholz, Louis, et al.
Publicado: (2024)

Checkification: A Practical Approach for Testing Static Analysis Truths
por: Ferreiro, Daniela, et al.
Publicado: (2025)

Abstractions of Sequences, Functions and Operators
por: Rustenholz, Louis, et al.
Publicado: (2025)

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

Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)
por: Young, David, et al.
Publicado: (2024)

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
por: Foo, Darius, et al.
Publicado: (2023)

SSA without Dominance for Higher-Order Programs
por: Leißa, Roland, et al.
Publicado: (2026)

Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs
por: Xu, Han, et al.
Publicado: (2026)

Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
por: Nicola, Mihai, et al.
Publicado: (2024)

C*: Unifying Programming and Verification in C
por: Cao, Yiyuan, et al.
Publicado: (2025)

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
por: Faella, Marco, et al.
Publicado: (2024)

Towards Automated Verification of LLM-Synthesized C Programs
por: Mukherjee, Prasita, et al.
Publicado: (2024)

Bialgebraic Reasoning on Higher-Order Program Equivalence
por: Goncharov, Sergey, et al.
Publicado: (2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
por: Haselwarter, Philipp G., et al.
Publicado: (2024)

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

Practical Formal Verification for MLIR Programs
por: Tucker, Emily, et al.
Publicado: (2026)

HITrees: Higher-Order Interaction Trees
por: Ayyam, Amir Mohammad Fadaei, et al.
Publicado: (2025)

Higher Order Automatic Differentiation of Higher Order Functions
por: Huot, Mathieu, et al.
Publicado: (2021)

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

Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
por: Nagar, Kartik, et al.
Publicado: (2020)

Solvable Tuple Patterns and Their Applications to Program Verification
por: Kobayashi, Naoki, et al.
Publicado: (2025)

Higher-Order Behavioural Conformances via Fibrations
por: Urbat, Henning
Publicado: (2025)

ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses
por: Singh, Avaljot, et al.
Publicado: (2024)

Towards a Higher-Order Bialgebraic Denotational Semantics
por: Goncharov, Sergey, et al.
Publicado: (2026)

Resource Specifications for Resource-Manipulating Programs
por: Grannan, Zachary, et al.
Publicado: (2023)

Actegories, Copowers, and Higher-Order Message Passing Semantics
por: Cockett, Robin, et al.
Publicado: (2025)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
por: Aguirre, Alejandro, et al.
Publicado: (2024)

A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs
por: Rustenholz, Louis, et al.
Publicado: (2024)

QCP: A Practical Separation Logic-based C Program Verification Tool
por: Wu, Xiwei, et al.
Publicado: (2025)

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
por: Dane, Serra Z., et al.
Publicado: (2026)

Composing Automatic Differentiation with Custom Derivatives of Higher-Order Functions
por: Estep, Sam
Publicado: (2024)

Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
por: Yang, Zhixuan, et al.
Publicado: (2025)

Verification Algorithms for Automated Separation Logic Verifiers
por: Eilers, Marco, et al.
Publicado: (2024)

Higher-Order Asynchronous Effects
por: Ahman, Danel, et al.
Publicado: (2023)

KestRel: Relational Verification Using E-Graphs for Program Alignment
por: Dickerson, Robert, et al.
Publicado: (2024)

Weighted NetKAT: A Programming Language For Quantitative Network Verification
por: Acevedo, Emmanuel Suárez, et al.
Publicado: (2026)

Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report
por: Giunti, Marco, et al.
Publicado: (2025)

A Hybrid Approach to Semi-automated Rust Verification
por: Ayoun, Sacha-Élie, et al.
Publicado: (2024)