Quantified Decision Procedures & Interpolation f. Correction

In spite of all the effort that goes into verification, the design of integrated circuits has become so complex that critical bugs often make their way into in silicon. Since respins are prohibitively expensive for all but show- stopping bugs, there is often a need for software workarounds for hardware bugs in systems involving both hardware and software components. In QUAINT, we propose to develop automatic methods to construct such workarounds. We will study the repair problem from two sides. On the one hand, we will develop methods to model hardware bugs in such a way that the search for a software workaround is feasible. The tasks include fault localization and solving formulas for a valid repair. Following previous work, we view the repair problem as a game played by two players (the environment and the system) with opposite interests (to violate and to fulfill the specification, resp.). Thus, the repair problem will naturally result in formulas with quantifier alternations. However, modifications are needed to consider available hardware constraints. The second goal is to develop novel methods to evaluate such formulas efficiently and to extract repairs from them. Here, we will use our existing expertise in interpolation for function extraction and quantifier elimination to speed up QBF solving and to generate certificates that allow for efficient repairs. We will also study ways to move beyond the bit level, studying quantified formulas in other logics, in particular using equality logic and uninterpreted functions.

Writing correct software or hardware is very difficult and bugs can have major consequences. For instance, on 9 May 2015, a software problem caused a military Airbus A400M to crash, killing four crew members and injuring two. In order to prevent such disasters, we want to prove software and hardware correct. The classical approach is to first write software and then to prove it, but this seems wasteful. It is preferable to synthesize correct software automatically from a given specification. The synthesis problem is a very difficult one, but in QUAINT we have made significant progress towards making it real. We have focused on two aspects: one is the collaboration between humans and synthesis tools. We have built synthesis tools that automatically construct that part of a program that is particularly difficult for a programmer, but not the parts that are easy. We have also created very efficient synthesis tools by exploring the connection between synthesis and different logics and logic solvers. Our Taiwanese partners, experts in logic, were crucial to these efforts. Finally, the project has contributed to the education of two brilliant young PhD students who have now joined Austrian industry.