A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic

TL;DR

This paper introduces an improved sorted Datalog hammer that extends previous work to handle mixed real-integer arithmetic and more complex inequalities, enhancing verification of supervisor code with better performance and conciseness.

Contribution

The paper generalizes the Datalog hammer to mixed arithmetic and inequalities, reduces output size with soft typing, and integrates tools into a single executable for more effective supervisor verification.

Findings

Successfully verified supervisor code for automotive examples.

Enhanced performance on real-world benchmarks.

More concise modeling of supervisor code.

Abstract

In a previous paper, we have shown that clause sets belonging to the Horn Bernays-Sch\"onfinkel fragment over simple linear real arithmetic (HBS(SLR)) can be translated into HBS clause sets over a finite set of first-order constants. The translation preserves validity and satisfiability and it is still applicable if we extend our input with positive universally or existentially quantified verification conditions (conjectures). We call this translation a Datalog hammer. The combination of its implementation in SPASS-SPL with the Datalog reasoner VLog establishes an effective way of deciding verification conditions in the Horn fragment. We verify supervisor code for two examples: a lane change assistant in a car and an electronic control unit of a supercharged combustion engine. In this paper, we improve our Datalog hammer in several ways: we generalize it to mixed real-integer arithmetic and finite first-order sorts; we extend the class of acceptable inequalities beyond variable bounds and positively grounded inequalities; and we significantly reduce the size of the hammer output by a soft typing discipline. We call the result the sorted Datalog hammer. It not only allows us to handle more complex supervisor code and to model already considered supervisor code more concisely, but it also improves our performance on real world benchmark examples. Finally, we replace the before file-based interface between SPASS-SPL and VLog by a close coupling resulting in a single executable binary.