Fri 12 Jan 2018 10:55 - 11:20 at Bunker Hill - Testing and Verification Chair(s): Santosh Nagarakatte

Random testing has proven to be an extremely effective way to catch subtle bugs in distributed systems in the presence of network partition faults. This is surprising, as the space of potentially faulty executions is enormous, and the bugs depend on a subtle interplay between sequences of operations and faults.

We provide a theoretical justification of the effectiveness of random testing in this context. First, we show a general construction, using the probabilistic method from combinatorics, that shows that whenever a random test covers a fixed coverage goal with sufficiently high probability, there is a small set of random tests which achieves full coverage with high probability. In particular, we show that our construction can give test sets exponentially smaller than systematic enumeration. Second, based on an empirical study of many bugs found by random testing in production distributed systems, we introduce notions of test coverage relating to network partition faults which are effective in finding bugs. Finally, we show using combinatorial arguments that for these notions of test coverage we introduce, we can find a lower bound on the probability that a random test covers a given goal. Our general construction then explains why random testing tools achieve good coverage—and hence, find bugs—quickly.

While we formulate our results in terms of network partition faults, our construction provides a step towards rigorous analysis of random testing algorithms. We demonstrate that several other random testing approaches in the literature can be explained using our main result.

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
Testing and VerificationResearch Papers at Bunker Hill
Chair(s): Santosh Nagarakatte Rutgers University, USA
10:30
25m
Talk
Generating Good Generators for Inductive Relations
Research Papers
Leonidas Lampropoulos University of Pennsylvania, Zoe Paraskevopoulou Princeton University, Benjamin C. Pierce University of Pennsylvania
10:55
25m
Talk
Why is Random Testing Effective for Partition Tolerance Bugs?
Research Papers
Rupak Majumdar MPI-SWS, Filip Niksic MPI-SWS
11:20
25m
Talk
On Automatically Proving the Correctness of math.h Implementations
Research Papers
Wonyeol Lee Stanford University, Rahul Sharma Microsoft Research, Alex Aiken Stanford University
11:45
25m
Talk
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Research Papers
Shelly Grossman Tel Aviv University, Ittai Abraham VMWare Research, Guy Gueta VMWare Research, Yan Michalevsky Stanford University, Noam Rinetzky Tel Aviv University, Mooly Sagiv Tel Aviv University, Yoni Zohar Tel Aviv University