Verification of programs with ADTs using Shallow Horn Clauses
This program is tentative and subject to change.
Thispaperconsidersverificationofrelationalpropertiesofprograms over algebraic data types (ADTs) by translating programs and properties into Constrained Horn clauses (CHCs). Verification reduces to satisfiability of CHCs modulo the theory of algebraic data types, which can be done by exhibiting a Herbrand model of the clauses. Herbrand models of CHCs with recursive ADTs are unbounded, so we need a formalism to finitely represent such models. We propose Shallow Horn Clauses (SHoCs), a new formalism for finitely representing unbounded Herbrand models. SHoCs enjoy the usual Boolean closure properties and are strictly more expressive and compact than tree automata and convoluted tree automata, which have previously been used for this purpose. We propose an iterative procedure for inferring SHoCs. The model inference problem arising from relational verification is undecidable, so we propose an incomplete but sound inference procedure. Experiments show that this procedure performs well in practice w.r.t. state of the art tools, both for verifying properties and for finding counterexamples.
This program is tentative and subject to change.
Mon 21 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30 | |||
11:00 30mFull-paper | Verification of programs with ADTs using Shallow Horn Clauses SAS | ||
11:30 30mFull-paper | An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants SAS Louis Rustenholz Universidad Politécnica de Madrid (UPM) and IMDEA Software Institute, Pedro López-García IMDEA Software Institute, José Morales IMDEA Software Institute, Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute Link to publication Pre-print | ||
12:00 30mFull-paper | Static Analysis of Quantum Programs SAS Nicola Assolini Università degli Studi di Verona, Alessandra Di Pierro University of Verona, Italy, Isabella Mastroeni University of Verona, Italy |