A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic

TL;DR

This paper introduces a method to translate certain logical verification conditions into a Datalog framework, enabling effective verification of complex systems like vehicle controllers using a new toolchain.

Contribution

It presents a novel translation approach for BS(SLR) clause sets into a finite constant set and a Datalog hammer for the Horn case, improving verification processes.

Findings

Effective translation of BS(SLR) clauses into finite constants.

A Datalog hammer that preserves validity and satisfiability.

Successful verification of automotive control systems.

Abstract

The Bernays-Sch\"onfinkel first-order logic fragment over simple linear real arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR) clause sets with both universally and existentially quantified verification conditions (conjectures) can be translated into BS(SLR) clause sets over a finite set of first-order constants. For the Horn case, we provide a Datalog hammer preserving validity and satisfiability. A toolchain from the BS(LRA) prover SPASS-SPL to the Datalog reasoner VLog establishes an effective way of deciding verification conditions in the Horn fragment. This is exemplified by the verification of supervisor code for a lane change assistant in a car and of an electronic control unit for a supercharged combustion engine.