Anzeige
Erschienen in:
2018 | OriginalPaper | Buchkapitel
Model Checking Procedural Programs
verfasst von : Rajeev Alur, Ahmed Bouajjani, Javier Esparza
Erschienen in: Handbook of Model Checking
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We consider the model-checking problem for sequential programs with procedure calls. We first present basic algorithms for solving the reachability problem and the fair computation problem. The algorithms are based on two techniques: summarization, which computes reachability information by solving a set of fixpoint equations, and saturation, which computes the set of all reachable program states (including call stacks) using automata. Then, we study formalisms to specify requirements of programs with procedure calls. We present an extension of Linear Temporal Logic allowing propagation of information across the hierarchical structure induced by procedure calls and matching returns. Finally, we show how model checking can be extended to this class of programs and properties.