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 |