Name
Abstract | ||
|---|---|---|
The combination of static and dynamic software analysis, such as data flow analysis (Dfa) and model checking, provides benefits for both disciplines. On the one hand, the information extracted by Dfas about program data may be utilized by model checkers to optimize the state space representation. On the other hand, the expressiveness of logic formulas allows us to consider model checkers as generic data flow analyzers. Following this second approach, we propose in this paper an algorithm to calculate Dfas using on-the-fly resolution of boolean equation systems (Bess). The overall framework includes the abstraction of the input program into an implicit labeled transition system (Lts), independent of the program specification language. Moreover, using Bess as an intermediate representation allowed us to reformulate classical Dfas encountered in the literature, which were previously encoded in terms of @m-calculus formulas with forward and backward modalities. Our work was implemented and integrated into the widespread verification platform Cadp, and experimented on real examples. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1016/j.entcs.2007.09.006 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
on-the-fly data flow analysis,program data,labeled transition system,boolean equation system,program specification language,verification technology,classical dfas,data flow analysis,input program,model checker,model checking,generic data flow analyzer,dynamic software analysis,intermediate representation,data flow,information extraction,software analysis,state space representation | Abstraction,Model checking,Programming language,Computer science,Software analysis pattern,State-space representation,Data-flow analysis,Theoretical computer science,Boolean algebra,Labeled transition system,Data flow diagram | Journal |
Volume | Issue | ISSN |
190 | 4 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
6 | 0.42 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| María del Mar Gallardo | 1 | 141 | 13.16 |
| Christophe Joubert | 2 | 21 | 2.41 |
| Pedro Merino | 3 | 201 | 25.98 |