A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic

Martin BrombergerMartin Bromberger, Irina DragosteIrina Dragoste, Rasha FaqehRasha Faqeh, Christof FetzerChristof Fetzer, Markus KrötzschMarkus Krötzsch, Christoph WeidenbachChristoph Weidenbach

Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach
A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
In Boris Konev, Giles Reger, eds., Proc. of the 13th Int. Symp. on Frontiers of Combining Systems (FROCOS 2021), volume 12941 of LNCS, 3-24, 2021. Springer

Details
Bibtex

KurzfassungAbstract
The Bernays-Schönfinkel 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.
Projekt:Project: CPEC, ScaDS.AI, Cfaed
Forschungsgruppe:Research Group: Wissensbasierte SystemeKnowledge-Based Systems

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-030-86205-3_1.

@inproceedings{BDFFKW2021,
  author    = {Martin Bromberger and Irina Dragoste and Rasha Faqeh and Christof
               Fetzer and Markus Kr{\"{o}}tzsch and Christoph Weidenbach},
  title     = {A Datalog Hammer for Supervisor Verification Conditions Modulo
               Simple Linear Arithmetic},
  editor    = {Boris Konev and Giles Reger},
  booktitle = {Proc. of the 13th Int. Symp. on Frontiers of Combining Systems
               (FROCOS 2021)},
  series    = {LNCS},
  volume    = {12941},
  publisher = {Springer},
  year      = {2021},
  pages     = {3-24},
  doi       = {10.1007/978-3-030-86205-3_1}
}