Item

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.