Abstract: Automated abstraction is a key technology in extending computer-aided verification methods to larger and more complex systems. In general terms, given a system and a property to prove, abstraction means extracting a simple set of facts about the system that are sufficient to prove the property. In this talk, we will see that this notion of abstraction is closely related to Craig's interpolation lemma. This is a classical result about predicate logic connecting proofs and abstraction. The lemma states that if formula A implies formula B, then there is an interpolant formula A' such that A implies A' and A' implies B, and such that A' is expressed over the common symbols of A and B. In some sense, the interpolant is an abstraction of A sufficient to prove BAutomated abstraction is a key technology in extending computer-aided verification methods to larger and more complex systems. In general terms, given a system and a property to prove, abstraction means extracting a simple set of facts about the system that are sufficient to prove the property. In this talk, we will see that this notion of abstraction is closely related to Craig's interpolation lemma. This is a classical result about predicate logic connecting proofs and abstraction. The lemma states that if formula A implies formula B, then there is an interpolant formula A' such that A implies A' and A' implies B, and such that A' is expressed over the common symbols of A and B. In some sense, the interpolant is an abstraction of A sufficient to prove B.

Robert Baillargeon has over a decade of experience in electrical/electronic automotive systems. He has worked in the Vehicle Electronics domain performing algorithm, software, methodology, process, and tools development. He is currently a Staff Researcher at General Motors Research, where he is the Thrust Area Leader for Electronics, Controls, and Software Process, Methods and Tools. He has a BS in Electrical Engineering from Michigan Technological University and a MS in Information Technology-Software Engineering from Carnegie Mellon University. Appointments: dcm@cs.cmu.edu