A method, postdomination, used to reduce the space requirements of data flow analysis (DFA) was discussed. A formal proof system was used that contained an approximation of the information collected at nodes when all paths were executed. The Java bytecode verification in particular fit the requirements and the proposed algorithm was used to develop a Verifier on memory limited embedded systems. The approach used has the potential to be feasible for a large number of programs, for a given amount of RAM, since the maximum nesting depth is largely independent from the total number of control instructions.
|Autori:||BERNARDESCHI C; LETTIERI G; MARTINI L; MASCI P|
|Titolo:||Using postdomination to reduce space requirements of data flow analysis|
|Anno del prodotto:||2006|
|Digital Object Identifier (DOI):||10.1016/j.ipl.2005.11.017|
|Appare nelle tipologie:||1.1 Articolo in rivista|