SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis
 by Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl & Yassine Lakhnech.

Abstract
We address the problem of verifying systems operating on different types of variables ranging over infinite domains. We consider in particular systems modeled by means of extended automata communicating through unbounded fifo channels. We develop a general methodology for analyzing such systems based on combining automatic generation of abstract models (not necessarily finite-state) with symbolic reachability analysis. Reachability analysis procedures allow to verify automatically properties at the abstract level as well as to generate auxiliary invariants and accurate abstraction functions that can be used at the concrete level. We propose a realization of this approach in a framework which extends PVS with automatic invariant checking strategies, automatic procedures for generating abstract models, as well as automata-based decision procedures and reachability analysis procedures for fifo channels systems.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy