2021/07/07 by Martin Bromberger, Irina Dragoste, Bromberger, Martin +9
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Reliability and Analysis Research
paper · pdf · doi:10.48550/arxiv.2107.03189
openalex publication_date 2021/07/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The Bernays-Sch "onfinkel first-order logic fragment over simple linear real\narithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR)\nclause sets with both universally and existentially quantified verification\nconditions (conjectures) can be translated into BS(SLR) clause sets over a\nfinite set of first-order constants. For the Horn case, we provide a Datalog\nhammer preserving validity and satisfiability. A toolchain from the BS(LRA)\nprover SPASS-SPL to the Datalog reasoner VLog establishes an effective way of\ndeciding verification conditions in the Horn fragment. This is exemplified by\nthe verification of supervisor code for a lane change assistant in a car and of\nan electronic control unit for a supercharged combustion engine.\n