Rescheduled: Reasoning about Critical Systems using Refinement

  • Date Friday, August 24, 2018  Time 11:00 AM
  • Speaker Pete Manolios
  • Location Galois Inc., 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)
  • Galois is pleased to host the following tech talk.
    These talks are open to the interested public--please join us!
    (There is no need to pre-register for the talk.)

    This talk will also be live streamed on our YouTube channel

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.