Graph-theoretic Properties of Control Flow Graphs and Applications
Neeraj Kumar · UWSpace (University of Waterloo) · 2015
I hereby declare that I am the sole author of this thesis. This is a true copy of the thesis, including any required final revisions, as accepted by my examiners. I understand that my thesis may be made electronically available to the public. ii This thesis deals with determining appropriate width parameters of control flow graphs so that certain computationally hard problems of practical interest become efficiently solv-able. A well-known result of Thorup states that the treewidth of control flow graphs arising from structured (goto-free) programs is at most six. However, since a control flow graph is inherently directed, it is very likely that using a digraph width measure would give better algorithms for problems where directional properties of edges are important. One such problem, parity game, is closely related to the µ-calculus model checking problem in software verification and is known to be tractable on graphs of bounded DAG-width, Kelly-width or entanglement. Motivated by this, we show that the DAG-width of control flow graphs arising from structured programs is at most three and give a linear-time algorithm to compute the corresponding DAG decomposition. Using similar techniques, we show that Kelly-width of control flow graphs is also bounded by three. Additionally, we also show that control flow graphs can have unbounded entanglement. In light of these results, we revisit the complexity of the µ-calculus model checking problem on these special graph classes and show that we can obtain better running times for control flow graphs. iii Acknowledgements I am extremely grateful to my supervisors Therese Biedl and Sebastian Fischmeister for their guidance and support over these two years. It has been a great learning experience and has played a pivotal role in shaping my career. I would also like to thank Naomi Nishimura and Werner Dietl for being on my thesis committee. I am also grateful to my friends here in Waterloo for all the good times and to my family for being so supportive of my academic endeavours. iv