Case Studies

The following table gives a summary of what Heap-Hop was able to verify on some case studies. We are interested in three properties:

CO
True if the communications in the program obey the contracts.
MFF
True if the program is memory-fault free.
LF
True if the program could be certified memory-leak free.

Experiments include copyless list transfer, service provider protocols, and load-balancing parallel tree disposal.

Program Contracts #LOC CO MFF LF
send_list_bug C 62 Y N Y
send_list_dualized C 48 Y Y N
send_list C 61 Y Y Y
send_list_leaking C 41 Y Y N
send_list_no_ack C 50 Y Y Y
send_list_non_det C 60 Y Y N
send_list_simple C 36 Y Y Y
simple_service_provider Ftp, Http, Service, Services 70 Y Y N
tcp2 Delegating, Listening, Serving 106 Y Y Y
tcp Listening, Serving 83 Y Y Y
load-balancing-tree-disposal2 C 65 Y Y N
load-balancing-tree-disposal C 129 Y Y N
spawning-threads-tree-disposal C 115 Y Y Y
shared_reads 16 Y Y Y
shared_msg C 37 Y Y Y