Abstract:
Verification is often the dominant cost in the design of critical systems. In this talk, we advocate the use of refinement to reason about critical systems. The idea is that a system is correct if all of its observable behaviors are allowed by an abstract system that acts as the specification. For example, to verify a microprocessor using refinement, one shows that it implements its instruction set architecture. We provide a general introduction to refinement and motivate the need for various notions of refinement. We present various techniques and methods that have been developed to facilitate mechanized reasoning. We discuss the use of refinement for reasoning about distributed systems and hardware.
Bio:
Pete Manolios is a Professor in the College of Computer and Information Science at Northeastern. Pete’s primary research interest is mechanized formal verification and validation of computational systems. Pete has served as an Associate Editor of ACM Transactions on Design Automation of Electronic Systems (TODAES), as a member of the FMCAD, ACL2 and ITP Steering Committees, and is a member of the IFIP working group 1.9/2.15 on Verified Software.