Interprocedural control flow graph

Here is a paper which has an example of interprocedural control flow graph among other things.

Computation of Interprocedural Control dependence by Harrold, Rothermel, and Sinha

Published in 1998 ACM SIGSOFT

Constant Propagation through procedures

Interprocedural Constant Propagation: A Study of Jump Function Implementations by Dan Grove(Sun Microsystems) and Linda Torczon(Rice Univ).

Published at SIGPLAN 1993

Abstract:

An implementation of interprocedural constant propagation must model the transmission of values through each procedure. This framework is modeled by a jump function. This paper reports on a comparative study of jump function implementations. It shows that different jump functions produce different numbers of useful constants; its suggests a particular function, called the pass-through parameter jump function, as the most cost-effective in practice

Static Analysis for Memory Operations

An Efficient Static Analysis Algorithm to Detect Redundant Memory Operations by Keith D. Cooper and Li Xu

Published at ACM 2002

Part of the Abstract:

As memory system performance becomes an increasingly dominant factor in overall system performance, it is important to optimize programs for memory related operations. This paper concerns static analysis to detect redundant memory operations and enable other compiler transformation to remove such redundant operations.

Hybrid Petri Net Representation of Gene Regulatory Network

This paper exploits a hybrid Petri Nets for representing gene regulatory networks. A hierarchial approach with HPNs makes easier the arrangment of the components in the gene regulatory network based on the biological facts and provides a prospective view of the network.

Reason for using Hybrid Petri nets: Representing a continous value such as a concentration of mRNA or protein is an essential factor in expressing gene regulation. Can do it only with HPN. It allows to handle the continous factor.

Modeling of metabolic pathways, extracellular and intracellular signaling pathways, or gene regulatory networks.

Things that you need to do:
Model discrete values : is certain protein present or not
Model continous values : like concentrations of certain things
Account for time delays associated with transitions ( time it takes to transcribe a gene or something)
Speed of the transitions that can take place.
Associate probabilities of the transition taking place.
This makes two kinds of transitions discrete and continuous (I don't really know what a continous trasition really means)
Something to represent the feedback mechanism ( this is key)
Also need to account for the Protein Protein Interaction
Protein DNA Interaction: Postive of Negative Effect on the synthesis of the protein associated
with a gene.
Solutions and Reactions and Enzymes
Dynamics of the reaction. (forward or backward)
Paper for that


Things that can be used to model these things
Hybrid Petri Nets
Hybrid Automatos
mu-calculus.

Modeling and querying biomolecular interaction networks

This is an interesting paper I found Click Here

The references of this paper might also be interesting and can lead to some background for us to start with.

Symbolic model Checking of biological systems

This is a poster on ideas for symbolic model checking of biological systems.

Poster

Model Checking Biological Systems

N. Kam, D. Harel, H. Kugler, R. Marelly, A. Pnueli, E.J.A Hubbard, and M.J. Stern: "Formal Modeling of C. elegans Development: A Scenario Based Approach ". In G.Ciobanu, G. Rozenberg (Eds.): ?Modeling in Molecular Biology?, pages 151-173, Natural Computing Series, Springer 2004.

N. Kam, I.R. Cohen, D. Harel: The Immune System as a Reactive System: Modeling T Cell Activation with Statecharts . To appear in Bull. Math. Bio.
An extended abstract of this paper appeared in Proc. Symposia on Human-Centric Computing Languages and Environments, pages 15-22, Stresa, Italy, September 2001. IEEE, © IEEE Computer Society Press

N. Kam, D. Harel, and I.R. Cohen. Modeling biological reactivity: Statecharts vs. boolean logic. In Proc. 2nd International Conference on Systems Biology, Pasadena, CA, USA, November 2001

Detecting infeasible paths statically

Refining Data Flow Information using Infeasible Paths : Published in the Fifth ACM SIGSOFT Symposium on Foundations of Software Engineering and Sixth European Software Engineering Conference in 1997. By Rastislav Bodik, Rajiv Gupta and Mary Lou Soffa.

Key points of the paper.

1. Some of the paths in a program are infeasible and will never be executed. In data flow testing, imprecision may lead to the selection of def-use pairs which are impossible to test because they lie on infeasible paths.

2. A conditional branch has a static co-relation along a path if its outcome can be determined along the path from prior statements or branch outcomes at compile time. Experiments show that from 9-40% of conditionals in large programs exhibit correlation that is detectable at compile time.

They present an alogrithm for the detection of branch co-rrelation and identification of infeasible program sub-paths and then they present the def-use pair analysis that excludes def-use pairs spanning the identified infeasible subpaths.

Control Flow Graph

Building a Control-flow Graph from Scheduled Assembly Code

This paper presents an algorithm for building correct CFGs from scheduled assembly code that includes branches in branch delay slots. The algorithm works by building an approximate CFG
and then refining it to reflect the actions of delayed branches.

Excerpts from the paper that I think are important to understand the paper

-- The control flow graph (CFG) is a fundamental data structure needed by almost all the techniques that compilers use to find oppurtunities for optimization and to prove the safety of these
optimizations. Such analysis includes

global data flow analysis
construction of a SSA graph
data dependence analysis.

--Branches that target an address held in a register (as opposed to an immediate constant) introduce a level of uncertainty that produces spurious edges in the CFG.
Add an edge from the block containing the branch to every block that it might reach.

The compiler can narrow the set by finding all the labels that the program loads into registers. This is safe unless the program performs arithmetic on a label value and branches to the result.

For a more precise analysis : Call-graph construction with function-valued parameters. (Cross Reference this)

Base Algorithm:
The first step partitions the code into a set of basic blocks (single assembly instruction)
These become the nodes in the CFG. THe second step looks at the branches in the code and fills in
the CFG's edges to represent the flow of control.

To show the exploration algorithm can use the style presented in the page 4 of this paper.
Do we assume that branches only see target labels and not arbitary PC addresses???