Refining the control structure of loops using static analysis

Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivančić, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationEmbedded Systems Week 2009 - Proceedings of the 7th ACM International Conference on Embedded Software, EMSOFT '09
Pages49-58
Number of pages10
DOIs
StatePublished - Dec 24 2009
Externally publishedYes
EventEmbedded Systems Week 2009, ESWEEK 2009 - 7th ACM International Conference on Embedded Software, EMSOFT '09 - Grenoble, France
Duration: Oct 11 2009Oct 16 2009

Publication series

NameEmbedded Systems Week 2009 - Proceedings of the 7th ACM International Conference on Embedded Software, EMSOFT '09

Other

OtherEmbedded Systems Week 2009, ESWEEK 2009 - 7th ACM International Conference on Embedded Software, EMSOFT '09
CountryFrance
CityGrenoble
Period10/11/0910/16/09

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Abstract interpretation
  • Loop refinement
  • Model checking
  • Path-sensitive analysis
  • Program understanding
  • Program verification
  • Static analysis
  • Synchronous sytems

Fingerprint Dive into the research topics of 'Refining the control structure of loops using static analysis'. Together they form a unique fingerprint.

  • Cite this

    Balakrishnan, G., Sankaranarayanan, S., Ivančić, F., & Gupta, A. (2009). Refining the control structure of loops using static analysis. In Embedded Systems Week 2009 - Proceedings of the 7th ACM International Conference on Embedded Software, EMSOFT '09 (pp. 49-58). (Embedded Systems Week 2009 - Proceedings of the 7th ACM International Conference on Embedded Software, EMSOFT '09). https://doi.org/10.1145/1629335.1629343