Write a Blog >>
ASE 2020
Mon 21 - Fri 25 September 2020 Melbourne, Australia
Wed 23 Sep 2020 16:00 - 16:20 at Kangaroo - Testing (2) Chair(s): Alex Groce

Model counting is the problem for finding the number of solutions to a formula over a bounded universe. This is a classic problem in computer science that has seen many recent advances in techniques and tools that tackle it. These advances have led to applications of model counting in many domains, e.g., quantitative program analysis, reliability, and security. Given the sheer complexity of the underlying problem, today’s model counters employ sophisticated algorithms and heuristics, which result in complex tools that must be heavily optimized. Therefore, establishing the correctness of implementations of model counters necessitates rigorous testing. This experience paper presents an empirical study on testing industrial strength model counters by applying the principles of differential and metamorphic testing together with bounded exhaustive input generation and input minimization. We embody these principles in the TestMC framework, and apply it to test four model counters, including three state-of-the-art model counters from three different classes. Specifically, we test the exact model counters projMC and dSharp, the probabilistic exact model counter Ganak, and the probabilistic approximate model counter ApproxMC. As subjects, we use three complementary test suites of input formulas. One suite consists of larger formulas that are derived from a wide range of real-world software design problems. The second suite consists of a bounded exhaustive set of small formulas that TestMC generated. The third suite consists of formulas generated using an off-the-shelf CNF fuzzer. TestMC found bugs in three of the four subject model counters. The bugs led to crashes, segmentation faults, incorrect model counts, and resource exhaustion by the solvers. Two of the tools were corrected subsequent to the bug reports we submitted based on our study, whereas the bugs we reported in the third tool were deemed by the tool authors to not require a fix.

Wed 23 Sep
Times are displayed in time zone: (UTC) Coordinated Universal Time

16:00 - 17:00: Testing (2)Research Papers at Kangaroo
Chair(s): Alex GroceNorthern Arizona University
16:00 - 16:20
TestMC: Testing Model Counters using Differential and Metamorphic TestingExperience
Research Papers
Muhammad UsmanUniversity of Texas at Austin, USA, Wenxi WangUniversity of Texas at Austin, USA, Sarfraz KhurshidUniversity of Texas at Austin, USA
16:20 - 16:40
BigFuzz: Efficient Fuzz Testing for Data Analytics using Framework Abstraction
Research Papers
Qian ZhangUniversity of California, Los Angeles, Jiyuan WangUniversity of California, Los Angeles, Muhammad Ali GulzarUniversity of California at Los Angeles, USA, Rohan PadhyeCarnegie Mellon University, Miryung KimUniversity of California at Los Angeles, USA
16:40 - 17:00
Scaling Client-Specific Equivalence Checking via Impact Boundary Search
Research Papers
Nick FengUniversity of Toronto, Vincent HuiUniversity of Toronto, Federico MoraUniversity of California, Berkeley, Marsha ChechikUniversity of Toronto