Proving Termination of C Programs with Lists

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.

Implementation in AProVE

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.

Web Interface

Our implementation can be tested via a web interface.

JAR File

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

Experiments

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