Cargando…

Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates

We address the problem of proving the satisfiability of Constrained Horn Clauses (CHCs) with Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs with ADTs into CHCs where predicates are defined over basic types, such as integers and booleans, only....

Descripción completa

Detalles Bibliográficos
Autores principales: De Angelis, Emanuele, Fioravanti, Fabio, Pettorossi, Alberto, Proietti, Maurizio
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324141/
http://dx.doi.org/10.1007/978-3-030-51074-9_6