Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
- title:
- Coverset Induction with Partiality and Subsorts: A Powerlist Case Study
- presenter:
- Joe Hendrix
- time:
- 10:30am, Tuesday, 22 June 2010.
- location:
- Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
- abstract:
-
Many inductive theorem provers use induction schemes derived from the recursive calls in functions definitions. This widely-used strategy is called coverset induction in the context of algebraic specifications. One challenge in applying coverset induction is that it typically requires using a total recursive function, while many operations on data structures are only meaningful on some well-formed subset of their possible inputs.
In this talk, I’ll discuss a generalization of coverset induction to handle partial constructors and operations. The generalization is implemented in the Maude ITP, and used in an extensive case study involving powerlists — a data structure introduced by J. Misra to elegantly formalize parallel algorithms based on divide and conquer strategy. Powerlists are constructed by partial operations, and it has been a challenge to naturally reason about powerlists using a formal logic that only supports total operations. We show how theorems about powerlists can be elegantly proven using the generalized coverset induction scheme implemented in the Maude ITP.
- bio:
- Joe is a member of the technical staff at Galois, Inc. He is interested in developing tools for making software development easier and safer. He started out developing software for civil engineers to analyze the safety of bridge foundations. He worked on automated decision procedures during his PhD at the University of Illinois. Immediately prior to joining Galois, he developed software within Microsoft’s Trustworthy Computing Initiative.