5 citations · 5 across the 2 of their papers we have counts for
3 papers · 1 filter
Saturating Sorting without Sorts
Pamina Georgiou, Márton Hajdu, Laura Kovács
We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formal…
Trace Logic for Inductive Loop Reasoning
Pamina Georgiou, Bernhard Gleiss, Laura Kovács
We propose trace logic, an instance of many-sorted first-order logic, to automate the partial correctness verification of programs containing loops. Trace logic generalizes semanti…
Verifying Relational Properties using Trace Logic
Gilles Barthe, Renate Eilers, Pamina Georgiou +3
We present a logical framework for the verification of relational properties in imperative programs. Our work is motivated by relational properties which come from security applica…