NASA Logo, National Aeronautics and Space Administration

+NASA Home

+Ames Home

Corina Pasareanu Wins IBM Haifa Verification Conference Best Paper Award
Intelligent Systems Division Banner

Corina Pasareanu Wins IBM Haifa Verification Conference Best Paper Award

Robust Software Engineering group member Corina Pasareanu (Carnegie Mellon University/SGT Inc.), was one of the authors of the paper, “Assume Guarantee Abstraction Refinement Meets Hybrid Systems,” which received the Best Paper Award at the 2014 IBM Haifa Verification Conference (HVC’14).

Authors (in alphabetical order): Sergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina Pasareanu, Andreas Podelski, and Thomas Strump

Abstract: Compositional verification techniques in the assume-guarantee style have been successfully applied to transition systems to efficiently reduce the search space by leveraging the compositional nature of the systems under consideration. We adapt these techniques to the domain of hybrid systems with affine dynamics. To build assumptions, we introduce an abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement. We have implemented our approach in the symbolic hybrid model checker SpaceEx. The evaluation shows its practical potential. To the best of our knowledge, this is the first work combining assume-guarantee reasoning with automatic abstraction-refinement in the context of hybrid automata.

BACKGROUND: HVC'14 is the tenth in the series of annual conferences dedicated to advancing the state-of the art and state-of-the-practice in verification and testing. The conference provides a forum for researchers and practitioners from academia and industry to share their work, exchange ideas, and discuss the future directions of testing and verification for hardware, software, and complex hybrid systems.

NASA PROGRAM FUNDING: System-wide Safety Assurance Technologies (SSAT) project, Aviation Safety Program (ASP), Aeronautics Research Mission Directorate (ARMD)

Contact: Corina Pasareanu

First Gov logo
NASA Logo -