VMCAI 2009: Case Studies

"tftp" (TFTP-HPA 0.48)

Source:: tftp.tar.gz (browse).
Logs:: Property A ("max. probability of establishing a write request"); Property B ("max. probability of successfully transferring some ﬁle data"); Property C ("max. expected amount of data that is sent before timeout")
Typical predicates (from fastest run of property B):: is_request == 0, sp == NULL, f < 0, return_value_pick_port_bind$1 == 0, connected == 0, host == NULL, fd < 0, size < 0, buffer.counter < 0, p - &dp$object.th_data[0] < 0, &dp$object.th_data[0] - &dp$object.th_data[0] < 0, n == 4 + size, (int)len == 4 + size, (int)((unsigned int)size) == size, (int)((unsigned int)return_value_makerequest$1) == return_value_makerequest$1, (int)((unsigned int)cp) + -(int)((unsigned int)((signed char *)tp)) == cp - (signed char *)tp, (int)((unsigned int)(&tp$object.th_u.tu_stuff[0])) + -(int)((unsigned int)((signed char *)tp)) == &tp$object.th_u.tu_stuff[0] - (signed char *)tp, (int)((unsigned int)(&tp$object.th_u.tu_stuff[0])) + -(int)((unsigned int)((signed char *)dp)) == &tp$object.th_u.tu_stuff[0] - (signed char *)dp, (int)((unsigned int)buffer.counter) == buffer.counter, (int)((unsigned int)p) + -((int)((unsigned int)(&dp$object.th_data[0]))) == p - &dp$object.th_data[0], (int)((unsigned int)(&dp$object.th_data[0])) + -((int)((unsigned int)(&dp$object.th_data[0]))) == &dp$object.th_data[0] - &dp$object.th_data[0], timeout >= 25, 5 + timeout >= 25, n < 0, 10 + timeout >= 25, (unsigned int)ap_opcode == 5, (unsigned int)((unsigned short int)ap$object.th_opcode) == 5, (unsigned int)ap_opcode == 4, (unsigned int)((unsigned short int)ap$object.th_opcode) == 4, size == 512, return_value_makerequest$1 == 516, cp - (signed char *)tp == 516, &tp$object.th_u.tu_stuff[0] - (signed char *)tp == 516, &tp$object.th_u.tu_stuff[0] - (signed char *)dp == 516, buffer.counter == 512, p - &dp$object.th_data[0] == 512, &dp$object.th_data[0] - &dp$object.th_data[0] == 512, (unsigned int)block == 1, (unsigned int)(1 + block) == 1, return_value_prob_bool_bias$3, tmp$2, pkt_at_svr == 0, 15 + timeout >= 25, 20 + timeout >= 25, 25 + timeout >= 25, 30 + timeout >= 25, return_value_prob_bool_bias$1, (unsigned int)dp_opcode == 2, (unsigned int)((unsigned short int)buf$object.th_opcode) == 2, (unsigned int)dp_opcode == 3, (unsigned int)((unsigned short int)buf$object.th_opcode) == 3

"ping" (GNU Inetutils 1.5)

Source:: ping.tar.gz (browse).
Logs:: Property A ("max. probability of not receiving a reply to an echo request"); Property B ("max. prob. of establishing connectivity with packet loss following two requests"); Property C ("max. expected number of echo requests required to establish connectivity")
Typical predicates (from fastest run of property B with predicate initialisation):: data_length >= 8, p.ping_num_recv == -1, 1 + p.ping_num_recv > 0, p.ping_num_xmit == 1, 1 + p.ping_num_recv >= 1 + p.ping_num_xmit, 1 + p.ping_num_xmit <= 1, (1 & options) == 0, preload == 0, (int (*)())(&echo_finish) == NULL, count <= 1, count == 0, p.ping_count == 0, p.ping_count <= 1, finish == NULL, finishing == 0, 1 + (unsigned int)p.ping_num_xmit >= p.ping_count, 1 + (unsigned int)p.ping_num_xmit >= count, 1 + (unsigned int)p.ping_num_xmit >= 2, p.ping_num_xmit == 0, 1 + p.ping_num_recv >= 2 + p.ping_num_xmit, 2 + p.ping_num_xmit <= 1, 2 + (unsigned int)p.ping_num_xmit >= p.ping_count, 2 + (unsigned int)p.ping_num_xmit >= count, 2 + (unsigned int)p.ping_num_xmit >= 2, 1 + (unsigned int)nresp >= p.ping_count, p.ping_num_xmit == -1, 1 + p.ping_num_recv >= 3 + p.ping_num_xmit, 3 + (unsigned int)p.ping_num_xmit >= p.ping_count, tmp$2 == 0, packet_out, p.ping_num_xmit == 2, 1 + p.ping_num_recv >= p.ping_num_xmit, (unsigned int)p.ping_num_xmit >= p.ping_count, p.ping_num_recv > 0, p.ping_num_recv >= p.ping_num_xmit, p.ping_num_recv >= 1 + p.ping_num_xmit, 1 + p.ping_num_xmit <= 0, p.ping_num_recv >= 2 + p.ping_num_xmit, p.ping_num_recv == 0, return_value_prob_bool_bias$1, n == 1, n < 0, (unsigned int)nresp >= p.ping_count, return_value_ping_recv$3 == 0, (int (*)())finish == &echo_finish, proto == NULL, fd < 0, return_value__socket$1 < 0, return_value_prob_bool_bias$1, 3 + p.ping_num_xmit <= 1, 1 + p.ping_num_recv >= 4 + p.ping_num_xmit, 2 + p.ping_num_recv > 0, 2 + p.ping_num_recv >= 2 + p.ping_num_xmit

"Herman" (APEX, 5 processes)

Source:: herman.tar.gz (browse).
Logs:: Property A ("min. probability of terminating in a stable state"); Property B ("max. expected number of rounds before termination")
Typical predicates (from fastest run of property B):: x[0], x[4], x[3], x[1], i == 0, x[1 + i], tmp, return_value_prob_bool$1, z, i == 3, i == 1, x[2], i == 2, token == 0, token == 2, i == 4, i < 4, 1 + i < 4, 2 + i < 4, i > 0, 1 + i > 0, x[-1 + i], x[-1], i == -1, x[i], x[2 + i], 3 + i < 4, i == -2, 2 + i > 0, x[3 + i], 4 + i < 4, i == -3, 3 + i > 0, x[4 + i], 5 + i < 4, i == -4, 4 + i > 0, x[5 + i], return_value_prob_bool$2, tmp

"IPv4 Zeroconf" (PRISM, K=4)

Source:: zeroconf.tar.gz (browse).
Logs:: Property A ("min. probability of conﬁguring with a fresh IP"); Property B ("max. expected number of probes")
Typical predicates (from fastest run of property A):: ip, (int)configured == 0, arp, k < 4, 1 + k < 4, 2 + k < 4, 3 + k < 4, 4 + k < 4, 5 + k < 4, (int)ip == 0, probe

"Bounded retransmission protocol" (PRISM, N=64, MAX=4)

Source:: brp.tar.gz (browse).
Logs:: Property A ("max. probability of the receiving nothing while a chunk was sent"); Property B ("max. probability of the sender reporting uncertainty")
Typical predicates (from fastest run of property B):: srep == 3, i < 64, 1 + i < 64, return_value_prob_bool$2, return_value_prob_bool$1, nrtr == 5, nrtr == 4