Translating flowcharts to non-deterministic languages
Pages 155 - 162
Abstract
Modeling languages are used to verify software and can be classified into deterministic modeling languages and non-deterministic modeling languages. Deterministic modeling languages have a single thread of control whereas non-deterministic ones have a multitude of threads of control and are more amenable for program transformations and analyses. However, deterministic languages such as control-flow graphs are pre-dominantly used in programming language tools.
In this work, we translate programs in a deterministic flowchart language to a non-deterministic algebraic modelling language. For the translation, we employ the technique of converting a finite state automata to a regular expression. The states of the finite state automata represent states in the control-flow graph, and the edges represent the edges in the control-flowgraph. We construct a homomorphism to show that the translation is sound, i.e., we prove that the semantics of the program in the deterministic flowchart language is preserved in the translation. Experiments on our implemented algorithm are conducted on the SPEC benchmark suite.
References
[1]
A. V. Aho, M. S. Lam, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Pearson Education, Inc, 2006.
[2]
C. Baier, J.-P. Katoen, and K. G. Larsen. Principles of Model Checking. The MIT Press, 2008.
[3]
T. Ball, E. Bounimova, R. Kumar, and V. Levin. Slam2: static driver verification with under 4% false alarms. In Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD '10, pages 35--42, Austin, TX, 2010. FMCAD Inc.
[4]
C. Böhm and G. Jacopini. Flow diagrams, Turing machines and languages with only two formation rules, pages 11--25. Yourdon Press, Upper Saddle River, NJ, USA, 1979.
[5]
C. Cifuentes. Reverse Compilation Techniques. PhD thesis, Queensland University of Technology, 1994.
[6]
K. Cooper and L. Torczon. Engineering a Compiler. Morgan Kaufmann Publisher, 2004.
[7]
S. P. E. Corporation. Spec cpu 2006. http://www.spec.org, 2006.
[8]
P. Cousot. Semantic foundations of program analysis. In S. Muchnick and N. D. Jones, editors, Program Flow Analysis. Prentice Hall, 1981.
[9]
D. Gopan and T. W. Reps. Lookahead widening. In T. Ball and R. B. Jones, editors, CAV, volume 4144 of Lecture Notes in Computer Science, pages 452--466. Springer, 2006.
[10]
S. Gulwani, S. Jain, and E. Koskinen. Control-flow refinement and progress invariants for bound analysis. In Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation, PLDI '09, pages 375--385, New York, NY, USA, 2009. ACM.
[11]
M. Handjieva and S. Tzolovski. Refining static analyses by trace-based partitioning using control flow. In G. Levi, editor, SAS, volume 1503 of Lecture Notes in Computer Science, pages 200--214. Springer, 1998.
[12]
G. Holzmann. The Spin Model Checker: primer and reference manual. Addison-Wesley Professional, 2003.
[13]
G. A. Kildall. A unified approach to global program optimization. In Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, POPL '73, pages 194--206, New York, NY, USA, 1973. ACM.
[14]
C. Lattner and V. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, CGO '04, pages 75--, Washington, DC, USA, 2004. IEEE Computer Society.
[15]
J. v. Leeuwen. Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics. Elsevier Science Publishers B. V., 1994.
[16]
J. Miecznikowski and L. J. Hendren. Decompiling java bytecode: Problems, traps and pitfalls. In Compiler Construction, 11th International Conference (CC), volume 2304 of phLecture Notes in Computer Science, pages 111--127, Grenoble, France, 2002. Springer.
[17]
P. H. Morris, R. A. Gray, and R. E. Filman. Goto removal based on regular expressions. Journal of Software Maintenance, 9: 47--66, February 1997.
[18]
A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 46--57, Washington, DC, USA, 1977. IEEE Computer Society.
[19]
X. Rival and L. Mauborgne. The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst., 29, August 2007.
[20]
R. E. Tarjan. Fast algorithms for solving path problems. J. ACM, 28: 594--614, July 1981.
[21]
R. E. Tarjan. A unified approach to path problems. J. ACM, 28: 577--593, 1981.
[22]
J. Ullman, J. Hopcroft, and R. Motwani. Introduction to Automata Theory, Languages, and Computation. Pearson Addison-Wesley, 2003.
Index Terms
- Translating flowcharts to non-deterministic languages
Recommendations
Deterministic Pushdown Automata and Unary Languages
CIAA '08: Proceedings of the 13th international conference on Implementation and Applications of AutomataThe simulation of deterministic pushdown automata defined over a one letter alphabet by finite state automata is investigated from a descriptional complexity point of view. We show that each unary deterministic pushdown automaton of size s can be ...
Deterministic and unambiguous two-dimensional languages over one-letter alphabet
The paper focuses on deterministic and unambiguous recognizable two-dimensional languages with particular attention to the case of a one-letter alphabet. The family DREC(1) of deterministic languages over a one-letter alphabet is characterized as both L(...
Generalizations of 1-deterministic regular languages
We examine two generalizations of 1-deterministic regular languages that are used for the content models of DTDs in XML. They are k-lookahead determinism and k-block-determinism. The k-lookahead determinism uses the first k symbols w"1w"2...w"k of the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2012
172 pages
Copyright © 2012 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 23 January 2012
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
POPL '12
Sponsor:
POPL '12: The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 23 - 24, 2012
Pennsylvania, Philadelphia, USA
Acceptance Rates
Overall Acceptance Rate 66 of 120 submissions, 55%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 145Total Downloads
- Downloads (Last 12 months)4
- Downloads (Last 6 weeks)1
Reflects downloads up to 11 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in