Presentations at LPAR-25

The research, conducted by Sophie Rain in collaboration with Lea Salome Brugger, Anja Petković Komel, Laura Kovács, and Michael Rawson, introduces CheckMate, a tool for automating the verification of game-theoretic security properties, with a particular focus on blockchain protocols. By utilizing automated reasoning techniques, CheckMate evaluates whether a game-theoretic protocol model is secure, ensuring Byzantine fault tolerance and incentive compatibility. The presentation detailed CheckMate’s input format, components, modes, and outputs. The tool was benchmarked using 15 different models, including decentralized protocols, board games, and game-theoretic examples.

SecInt student Marton Hajdu presented rewriting techniques based on reduction orderings that generate “just enough” consequences to maintain first-order completeness. This research, co-authored with Laura Kovács and Michael Rawson, focuses on enhancing superposition-based first-order theorem proving by using reduction orderings to strike a balance, ensuring first-order completeness. However, gaps were identified when applying this approach to inductive reasoning. As a result, the authors extended the superposition calculus with new rewriting-based techniques to generate the necessary consequences for automating induction in saturation, which is crucial for improving reasoning processes.

Marton also contributed to the research Sorting without Sorts, which addresses the functional correctness of programs using recursive data structures, with a specific focus on sorting algorithms. This work introduces a novel reasoning framework using many-sorted first-order logic to formalize the semantics of recursive programs, incorporating sortedness and permutation properties directly into the first-order formalization. Pamina Georgiou, Marton Hajdu, and Laura Kovács demonstrate the applicability of their framework on recursive sorting algorithms, including Mergesort and Quicksort.