This web site contains additional information on our article “Proving Termination of C Programs with Lists”. More precisely, we provide a longer version of our paper including all appendices, information on our implementation in the tool AProVE, and we describe our experiments.
The easiest way to run AProVE is via its web interface.
Moreover, recent releases of AProVE are available for download on GitHub. Release 3a3f7c8 is able to prove termination of C programs with linked lists. For termination analysis of C programs, the following dependencies have to be installed (see here for more installation instructions):
Extending the path environment is necessary so that AProVE can find these programs. For T2 resp. LoAT, the variable T2_PATH resp. LoAT_PATH has to be initialized to the path of the directory containing the tool.
In our implementation, we extended list invariants by additional components
c_i which can be integers or which are from the set
{?, < , <=, >, >= }
for all fields i from {1, …, n}.
They represent invariants for the contents of integer fields within a list invariant. For example, if c_i is <, then the values in
the i-th field are known to be sorted in ascending order. If c_i is an integer, then the values
are linearly increasing (or decreasing) by the addend c_i. This allows us to handle
examples where monotonic increase or decrease of the numbers in a list is crucial for
memory safety or termination (see the program with the function search
below).
In the following, we describe how to execute the implementation via the web interface and via the provided JAR file.
Our implementation can be tested via a web interface.
Enter Program Code
shows the program that is currently analyzed. The user can modify the program or replace it by a new one.Upload a File
of a program to analyze (where the file should have the extension .c
).Submit
calls AProVE in order to prove termination of the main()
function.Return to program input
takes you back to the web page with the input program.After downloading AProVE and installing all dependencies, make sure that the path variables are set as described above. Then AProVE can be run by executing
java -ea -jar aprove.jar -m wst myExample.c
To evaluate the power of our approach we tested it on the only two benchmark sets operating on linked lists that have been part of the C Termination categories of the software competitions SV-COMP and TermComp in 2022.
The first set consists of 18 C programs that have been added to the Termination category of SV-COMP in 2017. It can be found here. Nine of these programs are terminating. They are a collection of typical representative functions on lists. Two of the terminating programs only create a list of a given non-deterministic length recursively but they do not operate on the list afterwards. The remaining seven terminating programs first create a list and afterwards traverse the list, search a value in the list, or append two lists and compute the length afterwards. The programs contain several functions, where some of them use recursion. For many of them, the termination proof requires reasoning about the shape (e.g., the acyclicity) of the list.
In the table below, we compare our results to the results of UAutomizer from SV-COMP 2022. We tested AProVE using StarExec, which provides an Intel Xeon E5-2609 CPU with 2.4 GHz and 264 GB of RAM. For SV-COMP 2022, an Intel Xeon E3-1230 v5 CPU with 3.4 GHz and 33 GB of RAM was used. To make the results more comparable, we give the CPU times (instead of the wallclock times) and the maximum memory used in the table below. Here, the result YES
indicates a successful termination proof, the result NO
indicates a successful non-termination proof, and MAYBE
indicates that the tool crashed or terminated the verification process within the given time without a result.
Example Program | AProVE | CPU Time (s) | Memory (MB) | UAutomizer | CPU Time (s) | Memory (MB) |
---|---|---|---|---|---|---|
cll_by_lseg-alloca-1.c (NT) | NO | 14 | 1228 | MAYBE | 51 | 390 |
cll_by_lseg-alloca-2.c | YES | 28 | 1257 | YES | 20 | 420 |
cll_by_lseg_traverse-alloca.c (NT) | MAYBE | 24 | 1219 | NO | 24 | 380 |
cll_search-alloca-1.c | MAYBE | 69 | 1695 | MAYBE | 280 | 950 |
cll_search-alloca-2.c (NT) | NO | 36 | 1415 | NO | 21 | 390 |
cll_traverse-alloca.c (NT) | NO | 40 | 1406 | NO | 21 | 390 |
ll_append-alloca-1.c | YES | 76 | 1986 | MAYBE | 140 | 730 |
ll_append-alloca-2.c (NT) | MAYBE | 63 | 1607 | NO | 28 | 410 |
ll_append_rec-alloca-1.c | YES | 110 | 4755 | MAYBE | 180 | 800 |
ll_append_rec-alloca-2.c (NT) | MAYBE | 78 | 3034 | NO | 51 | 520 |
ll_create_rec-alloca-1.c (NT) | MAYBE | 30 | 1349 | MAYBE | 38 | 400 |
ll_create_rec-alloca-2.c | YES | 19 | 1277 | YES | 19 | 390 |
ll_search-alloca.c | YES | 42 | 1435 | MAYBE | 95 | 830 |
ll_search_not_found-alloca.c | YES | 38 | 1330 | MAYBE | 70 | 500 |
ll_traverse-alloca.c | YES | 34 | 1292 | MAYBE | 74 | 530 |
nondet_ll_search-alloca-1.c (NT) | NO | 48 | 1588 | NO | 43 | 500 |
nondet_ll_search-alloca-2.c | MAYBE | 90 | 1954 | MAYBE | 650 | 1300 |
nondet_ll_traverse-alloca.c (NT) | NO | 48 | 1696 | NO | 42 | 440 |
The second set also consists of 18 C programs and has been submitted to the TPDB by us in 2022 (this is the data base used in TermComp). This set can be found here. Two of the programs only create a list using recursion or a loop. Three of them traverse the list afterwards (by a loop, by recursion, or by a loop using explicit pointer arithmetic). Ten programs search for a certain value in the list. In contrast to the SV-COMP programs, for nine of these programs, not only the shape but also the contents of the list are relevant for proving termination. These programs differ in the contents of the created list, in the value that is searched for, or in the way the next list element is computed during the search.
For example, one program invokes the following function search
via
search(head, m%n)
, where m
contains
a non-deterministic non-negative value, n
contains a non-deterministic positive value, and head
points to a list of length n
containing the values n-1, n-2, ..., 0
.
void search(struct list* head, int i) {
struct list* curr = head;
while(curr->value != i) {
curr = curr->next;
}
}
Executing this function is only safe for lists that contain the searched value, so here
invariants for the contents of the integer fields are crucial for proving memory safety,
and thus, also for proving termination.
One of the ten programs uses explicit pointer arithmetic to access the fields of the list similar to our example program where offsetof
is used.
Finally, three programs perform common list operations such as inserting or deleting an element.
In the table below, we compare our results to the results of UAutomizer from TermComp 2022). Again, we tested AProVE using StarExec, which was also used for TermComp 2022. We give both the CPU times and the wallclock times for both tools. As above, the result YES
indicates a successful termination proof, the result NO
indicates a successful non-termination proof, and MAYBE
indicates that the tool crashed or terminated the verification process within the given time without a result.
In TermComp, a timeout of 300 seconds was used.
Example Program | AProVE | Wallclock (s) | CPU (s) | Memory (MB) | UAutomizer | Wallclock (s) | CPU (s) | Memory (MB) |
---|---|---|---|---|---|---|---|---|
asc_ll_search_last.c | YES | 8 | 25 | 1273 | timeout | 300 | 340 | 3500 |
cyclic_ll_search_last.c | MAYBE | 28 | 58 | 1481 | timeout | 300 | 341 | 2117 |
desc_ll_search-ptrdiff_existing.c | YES | 14 | 41 | 1405 | MAYBE | 5 | 12 | 364 |
desc_ll_search_existing.c | YES | 21 | 38 | 1360 | timeout | 300 | 350 | 2527 |
desc_ll_search_last.c | YES | 15 | 36 | 1331 | timeout | 300 | 343 | 2973 |
desc_ll_search_mod.c | YES | 13 | 42 | 1380 | timeout | 300 | 329 | 2299 |
desc_ll_with_offset_search.c | YES | 11 | 36 | 1321 | timeout | 300 | 355 | 2097 |
nondet_ll_delete.c | YES | 40 | 107 | 3073 | timeout | 300 | 353 | 2146 |
nondet_ll_init.c | YES | 8 | 26 | 1279 | YES | 9 | 21 | 496 |
nondet_ll_init_rec.c | YES | 7 | 19 | 1254 | timeout | 300 | 346 | 2496 |
nondet_ll_insert.c | YES | 17 | 48 | 1583 | timeout | 300 | 360 | 2089 |
nondet_ll_search_last_n.c | YES | 12 | 40 | 1387 | timeout | 300 | 335 | 2275 |
nondet_ll_search_last_zero.c | YES | 16 | 39 | 1411 | timeout | 300 | 334 | 2120 |
nondet_ll_search_zero.c | YES | 11 | 36 | 1355 | timeout | 300 | 346 | 2470 |
nondet_ll_skip.c | YES | 12 | 37 | 1358 | timeout | 300 | 336 | 2244 |
nondet_ll_traverse-ptrdiff.c | YES | 11 | 36 | 1310 | MAYBE | 5 | 11 | 368 |
nondet_ll_traverse.c | YES | 11 | 35 | 1292 | timeout | 300 | 340 | 3085 |
nondet_ll_traverse_rec.c | YES | 9 | 27 | 1310 | timeout | 300 | 342 | 1964 |