Open AccessData flow analysis as model checking
Author(s) -
Bernhard Steffen
Publication year - 1990
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v19i325.6715
Subject(s) - computer science , modal logic , model checking , modal , mathematical proof , algorithm , generator (circuit theory) , theoretical computer science , data flow diagram , construct (python library) , programming language , mathematics , power (physics) , chemistry , physics , geometry , quantum mechanics , database , polymer chemistry
The paper develops the idea that modal logic provides an appropriate framework for the specification of data flow analysis (DFA) algorithms as soon as programs are represented as models of the logic. This can be exploited to construct a DFA- generator that generates efficient DFA-algorithms from modal specifications by partially evaluating a specific model checker wrt the specifying modal formula. Moreover, the use of a modal logic as specification language for DFA-algorithms supports the compositional development of specifications and structured proofs of properties of DFA-algorithms. These ideas are applied to the problem of determining optimal computation points within flow graphs.