AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

Automated theorem provers (ATPs) are tools that automatically prove and disprove logical formulas. They are used as back-end reasoning tools in various applications, e.g., software verification, where they prove that your program has (no) bugs; program synthesis, where they automatically construct a program that satisfies a given specification; and as brute-force tactics in various interactive theorem provers, i.e., tools that assist humans in writing and formally checking proofs of theorems. Especially in the case of software verification, ATPs have to handle formulas over a combination of domain specific logics, also called theories. These theories typically correspond to data types found in programming languages, e.g., the theories of bit vectors, integers, and arrays. Luckily for us, many of these domains are closely related to other domains and problem classes for which we already have so called hammers, i.e., efficient and well-studied algorithms and tools. However, this still means that we have to turn screws into nails, i.e., transform one problem class into a domain for which a hammer exists.

In this talk, I will present three transformations that turn screws into nails. The first two transformations are the unit cube test and the bounding reduction for the theory of linear integer arithmetic. They allow our SMT (satisfiability modulos theories) solver SPASS-SATT to efficiently handle so called unbounded problems, on which other tools typically diverge. As a result, SPASS-SATT won several awards, is deemed as one of the best SMT solvers for linear arithmetic, and several of its techniques were re-implemented in other SMT solvers.

The third transformation is called a Datalog hammer and we use it in our tool SPASS-SPL to verify so called supervisors, i.e., components of technical systems that control their systems behavior. As a result of our Datalog hammer, we were able to verify supervisor code for two examples: a supervisor for lane change assistants in a car and an electronic control unit (ECU) of a supercharged combustion engine. The latter is of special interest because ECUs were hacked by car companies to cheat at emission tests and we hope that we can efficiently find these hacks with SPASS-SPL.

Jennifer Müller

+49 681 9325 2900

--email hidden

Zoom

997 1565 5535

passcode not visible

logged in users only