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.|
|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|
|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.