Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Bit-precise procedure-modular termination analysis
Chen H., David C., Kroening D., Schrammel P., Wachter B. ACM Transactions on Programming Languages and Systems40 (1):1-38,2018.Type:Article
Date Reviewed: Apr 27 2018

That software is pervasive in our lives is now a platitude. That much of this software is flawed has also reached the collective consciousness. A lot of code, much to the chagrin of most researchers in programming languages, is still written in ancient, unsafe languages like C. Practitioners take this in stride and forge ahead with tools to mitigate the problems incurred. One such problem is that of termination; that is, will a program (which is supposed to halt) do so? Of course, a misreading of the theory would say that writing such tools is “impossible.” The theory merely says that such tools are incomplete. Quite a lot of realistic code does seem to be within reach of well-crafted tools.

This paper is a well-written story of the design of such a tool by leveraging solid theory and following a thoroughly pragmatic approach to engineer a tool that will be practical. To anyone familiar with program analysis, there are absolutely no surprises here: this is not the story of a scientific breakthrough, but rather of the success of what science, engineering, and “craft” can achieve when melded together.

The paper itself proceeds in a very logical fashion: introducing the problem via small but motivating examples, setting up some preliminary definitions, giving a high-level (but precise) overview of the approach, elaborating on important details of their core contributions, outlining the implementation, giving results of thorough and well-crafted experiments, and highlighting some limitations and some routes forward. Not only is the code available on GitHub, but the authors have gone much further and provided a “reproducibility bundle,” a practice that many more authors should follow. (It is a little disappointing to see that, as of the writing of this review, there have been no updates to the code in four months, and some pull requests have not been dealt with.)

Anyone interested in termination analysis would benefit from reading this paper. Also, anyone interested in writing about tools would do well to read the paper and make sure that his own paper is as clear and thorough, not just in explanations, but also in providing enough information and code to make the results reproducible.

Reviewer:  Jacques Carette Review #: CR146008 (1807-0387)
Bookmark and Share
  Featured Reviewer  
 
Semantics Of Programming Languages (F.3.2 )
 
 
Program Analysis (F.3.2 ... )
 
 
Verification (D.4.5 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Semantics Of Programming Languages": Date
Contractions in comparing concurrency semantics
Kok J. (ed), Rutten J. Theoretical Computer Science 76(2-3): 179-222, 2001. Type: Article
Aug 1 1991
Abstract language design
Bradley L. Theoretical Computer Science 77(1-2): 5-26, 1990. Type: Article
Nov 1 1991
Determinism → (event structure isomorphism = step sequence equivalence)
Vaandrager F. Theoretical Computer Science 79(2): 275-294, 1991. Type: Article
Dec 1 1991
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy