@online{Bromberger_2107.03189,
TITLE = {A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic},
AUTHOR = {Bromberger, Martin and Dragoste, Irina and Faqeh, Rasha and Fetzer, Christof and Kr{\"o}tzsch, Markus and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2107.03189},
EPRINT = {2107.03189},
EPRINTTYPE = {arXiv},
YEAR = {2021},
ABSTRACT = {The Bernays-Sch\"onfinkel first-order logic fragment over simple linear real<br>arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR)<br>clause sets with both universally and existentially quantified verification<br>conditions (conjectures) can be translated into BS(SLR) clause sets over a<br>finite set of first-order constants. For the Horn case, we provide a Datalog<br>hammer preserving validity and satisfiability. A toolchain from the BS(LRA)<br>prover SPASS-SPL to the Datalog reasoner VLog establishes an effective way of<br>deciding verification conditions in the Horn fragment. This is exemplified by<br>the verification of supervisor code for a lane change assistant in a car and of<br>an electronic control unit for a supercharged combustion engine.<br>},
}