A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear 
Arithmetic

Bromberger, Martin; Dragoste, Irina; Faqeh, Rasha; Fetzer, Christof; Krötzsch, Markus; Weidenbach, Christoph

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Paper

A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic

MPS-Authors

/persons/resource/persons117832

Bromberger, Martin
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45719

Weidenbach, Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

arXiv:2107.03189.pdf
(Preprint), 632KB

Supplementary Material (public)

There is no public supplementary material available

Citation

Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., Krötzsch, M., & Weidenbach, C. (2021). A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. Retrieved from https://arxiv.org/abs/2107.03189.

Cite as: https://hdl.handle.net/21.11116/0000-0009-4A01-3

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.