Name
Abstract | ||
|---|---|---|
We introduce a novel approach to the automated termination analysis of computer programs: we use neural networks to represent ranking functions. Ranking functions map program states to values that are bounded from below and decrease as a program runs; the existence of a ranking function proves that the program terminates. We train a neural network from sampled execution traces of a program so that the network's output decreases along the traces; then, we use symbolic reasoning to formally verify that it generalises to all possible executions. Upon the affirmative answer we obtain a formal certificate of termination for the program, which we call a neural ranking function. We demonstrate that thanks to the ability of neural networks to represent nonlinear functions our method succeeds over programs that are beyond the reach of state-of-the-art tools. This includes programs that use disjunctions in their loop conditions and programs that include nonlinear expressions. |
Year | DOI | Venue |
|---|---|---|
2022 | 10.1145/3540250.3549120 | ACM SIGSOFT Conference on the Foundations of Software Engineering (FSE) |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mirco Giacobbe | 1 | 9 | 5.29 |
| Daniel Kroening | 2 | 3 | 3.08 |
| Julian Parsert | 3 | 1 | 2.06 |