A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
From International Center for Computational Logic
A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
Martin BrombergerMartin Bromberger, Irina DragosteIrina Dragoste, Rasha FaqehRasha Faqeh, Christof FetzerChristof Fetzer, Larry GonzálezLarry González, Markus KrötzschMarkus Krötzsch, Maximilian MarxMaximilian Marx, Harish K MuraliHarish K Murali, Christoph WeidenbachChristoph Weidenbach
Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K Murali, Christoph Weidenbach
A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
In Dana Fisman, Grigore Rosu, eds., Proc. of the 28th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), volume 13243 of LNCS, 480-501, 2022. Springer
A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
In Dana Fisman, Grigore Rosu, eds., Proc. of the 28th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), volume 13243 of LNCS, 480-501, 2022. Springer
- KurzfassungAbstract
In a previous paper, we have shown that clause sets belonging to the Horn Bernays-Schönfinkel fragment over simple linear real arithmetic (HBS(SLR)) can be translated into HBS clause sets over a finite set of first-order constants. The translation 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. We 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 paper, we improve our Datalog hammer in several ways: we generalize it to mixed real-integer arithmetic and finite first-order sorts; we extend the class of acceptable inequalities beyond variable bounds and positively grounded inequalities; and we significantly reduce 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. Finally, we replace the before file-based interface between SPASS-SPL and VLog by a close coupling resulting in a single executable binary. - Projekt:Project: CPEC, ScaDS.AI
- Forschungsgruppe:Research Group: Wissensbasierte SystemeKnowledge-Based Systems
@inproceedings{BDFFGKMMW2022,
author = {Martin Bromberger and Irina Dragoste and Rasha Faqeh and Christof
Fetzer and Larry Gonz{\'{a}}lez and Markus Kr{\"{o}}tzsch and
Maximilian Marx and Harish K Murali and Christoph Weidenbach},
title = {A Sorted Datalog Hammer for Supervisor Verification Conditions
Modulo Simple Linear Arithmetic},
editor = {Dana Fisman and Grigore Rosu},
booktitle = {Proc. of the 28th Int. Conf. on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS 2022)},
series = {LNCS},
volume = {13243},
publisher = {Springer},
year = {2022},
pages = {480-501},
doi = {10.1007/978-3-030-99524-9}
}
