Automated Formal Verification at the Hardware/Software Boundary

点击翻译按钮获取中文摘要

Computer chips, computer systems, and computer software are the most complex things ever designed by humans. For example, even the simple programs written by our students in their first computer science course have far more possible behaviors than there are photons in the universe! Not surprisingly, it's hard to get all the details right. In fact, companies now spend the most effort not on design, but on verification -- the task of determining if the system behaves correctly.******Formal verification is the use of mathematical logic to aid the verification process. My research emphasizes automatic formal verification, in which a computer program analyzes the system being designed, automatically finding bugs or proving properties about the design, with minimal human effort beyond specifying what is desired. Research breakthroughs over the past twenty years have made formal verification indispensible for verifying computer hardware -- all major computer companies use formal verification on their computer chips. This has been a big success story of academic research creating enormous value for society. With more recent research breakthroughs, automated formal verification is becoming mainstream for software verification as well.******Much of the impact of computing, however, comes not from hardware or software, per se, but from actual, life-changing, "smart" products -- the smartphone being the most obvious example, but with the coming Internet of Things, all sorts of everyday objects will become smart and connected. Smart products are the result of tightly integrated hardware and software, and it's obviously important to get this integration correct. However, companies are having great difficulty creating these new products, because hardware and software have fundamentally different models of computation, resulting in mistakes when integrating the two.******This proposal focuses on developing theoretical and practical tools for verifying the interaction between hardware and software. In some respects, this combines all of the challenges of automated formal verification of hardware and software, because verification must reason about both. On the other hand, I believe that there are certain characteristics and design patterns that can be exploited to enable practical, automatic formal verification at the hardware/software boundary. If successful, this research will generate a large quality and productivity boost for creating any smart product.**