Incremental SAT and SMT Reasoning for Scalable Verification

We are surrounded by computers, phones, smart devices and the applications (apps) running on them, day and night. These technologies became an essential part of our daily life, making it very important to gain assurance that they always work as intended. Formal verification provides techniques to show that a hardware or software system behaves exactly as it was originally planned, under all possible circumstances. Many of these verification techniques, for example model checking or symbolic execution, need to solve logical problems that are very similar to one another over and over again in order to show, or disprove, the correctness of a system. The focus of this project is on these underlying logical problems. Incremental solution methods try to exploit the similarity between the occurring logical problems in order to find solutions with less effort. The aim of this project is to introduce improved incremental solution methods to our logical problems, and thereby push the boundaries of formal verification techniques.

We use technology for almost everything - communication, transportation, work, shopping, entertainment, and more. But how can we be sure that the systems we rely on will always work properly? As we use more and more software and hardware, it becomes more and more important to make sure that they are correct. One way to achieve this is by describing their behavior using logical formulas and then using specialized automated reasoning tools to check if they function correctly in all possible situations. This project aimed to improve these reasoning tools by making them more efficient, versatile, and reliable. Over the past three years, we have made several key advancements. We introduced standardized ways for reasoning tools to work together, making them easier to use in larger systems and simplifying their future development and maintenance. We also developed new techniques to simplify complex logical problems - such as those describing hardware circuits - so they can be solved more efficiently. In addition, we invented a new approach to verify distributed protocols, rule sets that allow components of distributed systems to communicate with each other, by taking advantage of their built-in symmetries. To further increase trust in automated reasoning tools, we implemented new ways to ensure that the solutions they produce are correct and reliable. These improvements help advance the field of formal verification, making it easier and more efficient to prove that critical systems, such as medical devices or self-driving cars, function correctly and safely. By enhancing these verification tools, our research contributes to making everyday technology more dependable, reducing the risks of software failures and system malfunctions.