Skip to main content

Syntax-Guided Termination Analysis

Author(s): Fedyukovich, Grigory; Zhang, Yueling; Gupta, Aarti

To refer to this page use:
Abstract: We present new algorithms for proving program termination and non-termination using syntax-guided synthesis. They exploit the symbolic encoding of programs and automatically construct a formal grammar for symbolic constraints that are used to synthesize either a termination argument or a non-terminating program refinement. The constraints are then added back to the program encoding, and an off-the-shelf constraint solver decides on their fitness and on the progress of the algorithms. The evaluation of our implementation, called Freq-Term, shows that although the formal grammar is limited to the syntax of the program, in the majority of cases our algorithms are effective and fast. Importantly, FreqTerm is competitive with state-of-the-art on a wide range of terminating and non-terminating benchmarks, and it significantly outperforms state-of-the-art on proving non-termination of a class of programs arising from large-scale Event-Condition-Action systems.
Publication Date: 2018
Citation: Fedyukovich, Grigory, Yueling Zhang, and Aarti Gupta. "Syntax-Guided Termination Analysis." In International Conference on Computer Aided Verification (2018): pp. 124-143. doi:10.1007/978-3-319-96145-3_7
DOI: 10.1007/978-3-319-96145-3_7
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 124 - 143
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Computer Aided Verification
Version: Final published version. This is an open access article.

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.