LTL model checking for communicating concurrent programs
In Innovations in Systems and Software Engineering: a NASA journal (ISSE)
Abstract We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendez-vous between parallel threads with communicating pushdown systems (from now on CPDSs).The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed.