A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic

Talk by Martin Bromberger

Location: Online
Start: 31. March 2022 at 11:00 am
End: 31. March 2022 at 12:00 pm
Event series: Research Seminar Logic and AI
iCal

In a previous paper [1], we have shown that clause sets belonging to the Horn Bernays-Schönfinkel fragment over simple linear arithmetic (HBS(SLA)) can be translated into HBS clause sets over a finite set of first-order constants.

HBS clause sets are also called Datalog programs and HBS(SLA) can be seen as an extension of Datalog programs that allow simple arithmetic inequalities in the bodies of rules. The translation from HBS(SLA) to HBS 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. As a result, we were able to 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 talk, we present several new improvements to our Datalog hammer: we have generalized it to mixed real-integer arithmetic and finite first-order sorts; we extended the class of acceptable inequalities beyond variable bounds and positively grounded inequalities, and we significantly reduced 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.

References: [1] Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., Krötzsch, M., Weidenbach, C.: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic. In: Reger, G.,Konev, B. (eds.) Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, United Kingdom, September 8-10, 2021. Proceedings. Lecture Notes in Computer Science, vol. 12941, pp. 3–24. Springer (2021)

Online talk link:

https://bbb.tu-dresden.de/b/ali-zgz-l8d-52n