Dr. Corina Pasareanu is contributing a chapter on Compositional Reasoning to the Handbook of Model Checking. The book is being published by Springer and it is edited by professors Ed Clarke (Turing award winner), Tom Henzinger, and Helmuth Veith. It includes contributions from top researchers in the field.
The Handbook of Model Checking is intended to be the reference book in the field and the invitation to contribute a chapter to it is a sign of recognition for the work performed by Ames RSE researchers.
BACKGROUND: Over the past eight years, RSE researchers Corina Pasareanu and Dimitra Giannakopoulou have produced seminal work in the area of compositional reasoning. Compositional reasoning breaks down the verification of large systems into the verification of their components, which are smaller and therefore more amenable to verification. Corina and Dimitra developed the first fully automated compositional verification algorithm that is based on assume-guarantee reasoning; the algorithm uses learning techniques for the synthesis of assumptions needed in compositional proofs.
NASA PROGRAM FUNDING: ETDP
COLLABORATORS: Dimitra Giannakopoulou and Kedar Namjoshi (Bell Labs).
Contact: Corina Pasareanu