Refining the control structure of loops using static analysis

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Refining the control structure of loops using static analysis

Full text

Pdf (495 KB)

Source

International Conference on Compilers, Architecture and Synthesis for Embedded Systems archive
Proceedings of the seventh ACM international conference on Embedded software table of contents

Grenoble, France

SESSION: Analysis and verification table of contents

Pages 49-58

Year of Publication: 2009

ISBN:978-1-60558-627-4

Authors

Gogul Balakrishnan	NEC Labs America, Princeton, NJ, USA
Sriram Sankaranarayanan	NEC Labs America, Princeton, NJ, USA
Franjo Ivančić	NEC Labs America, Princeton, NJ, USA
Aarti Gupta	NEC Labs America, Princeton, NJ, USA

Sponsors

ACM: Association for Computing Machinery
SIGBED: ACM Special Interest Group on Embedded Systems
SIGMICRO: ACM Special Interest Group on Microarchitectural Research and Processing
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 20, Downloads (12 Months): 20, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1629335.1629343 What is a DOI?

ABSTRACT

We present a simple yet useful technique for refining the control structure of loops that occur in imperative programs. Loops containing complex control flow are common in synchronous embedded controllers derived from modeling languages such as Lustre, Esterel, and Simulink/Stateflow. Our approach uses a set of labels to distinguish different control paths inside a given loop. The iterations of the loop are abstracted as a finite state automaton over these labels. Subsequently, we use static analysis techniques to identify infeasible iteration sequences and subtract such forbidden sequences from the initial language to obtain a refinement. In practice, the refinement of control flow sequences often simplifies the control flow patterns in the loop. We have applied the refinement technique to improve the precision of abstract interpretation in the presence of widening. Our experiments on a set of complex reactive loop benchmarks clearly show the utility of our refinement techniques. Abstraction interpretation with our refinement technique was able to verify all the properties for 10 out of the 13 benchmarks, while abstraction interpretation without refinement was able to verify only four. Other potentially useful applications include termination analysis and reverse engineering models from source code.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Absint WCET timing analysis tool. http://www.absint.com/.
	2	Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. In Static Analysis Symposium (2003), vol. 2694 of LNCS, Springer, pp. 337--354.
	3	Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Wei, O., and Gupta, A. SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement. In SAS (2008), vol. 5079 of LNCS, pp. 238--254.
	4	Ball, T., and Rajamani, S. K. The SLAM toolkit. In CAV (2001), vol. 2102 of LNCS, pp. 260--264.
	5	Bardin, S., Finkel, A., Leroux, J., and Petrucci, L. FAST: Fast accelereation of symbolic transition systems. In CAV (July 2003), vol. 2725 of LNCS.
	6	Beyer, D., Henzinger, T. A., Jhala, R., and Majumdar, R. The software model checker BLAST. STTT 9, 5-6 (2007), 505--525.
	7	Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A., Monniaux, D., and Rival, X. A static analyzer for large safety-critical software. In PLDI (June 2003), pp. 196--207.
	8	Clarke, E., Kroening, D., and Lerda, F. A tool for checking ANSI-C programs. In TACAS (2004), vol. 2988 of LNCS.
	9	Colon, M., Sankaranarayanan, S., and Sipma, H. Linear invariant generation using non-linear constraint solving. In CAV (July 2003), vol. 2725 of LNCS, Springer, pp. 420--433.
	10	Colon, M., and Sipma, H. Synthesis of linear ranking functions. In Tools and Algorithms for Construction and Analysis of Systems (April 2001), vol. 2031 of LNCS.
	11	Cook, B., Podelski, A., and Rybalchenko, A. Termination proofs for systems code. In PLDI (2006).
	12	Cousot, P., and Cousot, R. Static determination of dynamic properties of programs. In Proc. ISOP'76 (1976), Dunod, Paris, France, pp. 106--130.
	13	Cousot, P., and Cousot, R. Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL (1977), pp. 238--252.
	14	Cousot, P., and Halbwachs, N. Automatic discovery of linear restraints among the variables of a program. In POPL'78 (Jan. 1978), pp. 84--97.
	15	Esparza, J., Hansel, D., Rossmanith, P., and Schwoon, S. Efficient algorithms for model checking pushdown systems. In CAV (2000), vol. 1855 of LNCS.
	16	Fehnker, A., Brauer, J., Huuck, R., and Seefried, S. Goanna: Syntactic software model checking. In Auto. Tech. for Verif. & Analysis (2008).
	17	Gaubert, S., Goubault, E., Taly, A., and Zennou, S. Static analysis by policy iteration on relational domains. In ESOP (2007), vol. 4421 of LNCS, pp. 237--252.
	18	Gawlitza, T., and Seidl, H. Precise fixpoint computation through strategy iteration. In ESOP (2007), vol. 4421 of LNCS, pp. 300--315.
	19	Gopan, D., and Reps, T. W. Lookahead widening. In CAV (2006), vol. 4144 of LNCS, pp. 452--466.
	20	Gopan, D., and Reps, T. W. Guided static analysis. In SAS (2007), vol. 4634 of LNCS, pp. 349--365.
	21	Goubault, E., and Putot, S. Static analysis of numerical algorithms. In SAS (2006), vol. 4134 of LNCS, Springer, pp. 18--34.
	22	Gulwani, S., Jain, S., and Koskinen, E. Control-flow refinement and progress invariants for bound analysis. PLDI 2009 (to appear).
	23	Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., and Xu, R.-G. Proving non-termination. In POPL (2008), ACM, pp. 147--158.
	24	Halbwachs, N. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993.
	25	Halbwachs, N., Proy, Y., and Roumanoff, P. Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11, 2 (1997), 157--185.
	26	Harary, F. Graph Theory. Addison-Wesley, 1969.
	27	Ivancic, F., Yang, Z., Ganai, M. K., Gupta, A., Shlyakhter, I., and Ashar, P. F-soft: Software verification platform. In CAV (2005), vol. 3576 of LNCS.
	28	Jeannet, B., Halbwachs, N., and Raymond, P. Dynamic partitioning in analyses of numerical properties. In Static Analysis Symposium, SAS'99 (Sep 1999), vol. 1694 of LNCS, pp. 39--50.
	29	MathWorks Inc. Electronic vehicle climate control simulink/stateflow model. www.mathworks.com/products/simulink/demos.html.
	30	Mathworks Inc. Simulink/stateflow (tm) model-based control design environment. Cf. www.mathworks.com/simulink.
	31	Mauborgne, L., and Rival, X. Trace partitioning in abstract interpretation based static analyzers. In ESOP (2005), vol. 3444 of LNCS, pp. 5--20.
	32	Min´e, A. A new numerical abstract domain based on difference-bound matrices. In PADO II (May 2001), vol. 2053 of LNCS, Springer, pp. 155--172.
	33	Sankaranarayanan, S., Ivancic, F., and Gupta, A. Program analysis using symbolic ranges. In SAS (2007), vol. 4634 of LNCS, pp. 366--383.
	34	Sankaranarayanan, S., Ivancic, F., Shlyakhter, I., and Gupta, A. Static analysis in disjunctive numerical domains. In SAS (2006), vol. 4134 of LNCS.
	35	Simon, A., and King, A. Widening polyhedra with landmarks. In APLAS (2006), vol. 4279 of LNCS.