Write a Blog >>
Mon 10 Jul 2017 16:25 - 16:50 at Bren 1414 - Symbolic Execution Chair(s): Gordon Fraser

The majority of Internet traffic is transferred by transport protocols. The correctness of these transport protocol implementations is hard to validate as their behaviors depend not only on their protocols but also on their network environments that can introduce dynamic packet delay and loss. Random testing, widely used in industry due to its simplicity and low cost, struggles to detect packet delay related faults which occur with low probability. Symbolic execution based testing is promising at detecting such low probability faults, but it requires large testing budgets as it attempts to cover a prohibitively large input space of packet dynamics. To improve its cost-effectiveness, we propose two domain-specific heuristic techniques, called packet retransmission based priority and network state based priority, which are motivated by two common transport protocol properties. In our experiments using the Linux TFTP programs, our techniques improve the cost-effectiveness of symbolic execution based testing for transport protocols, detecting three times as many faults when the budget is in the range of minutes and hours.

Mon 10 Jul

Displayed time zone: Tijuana, Baja California change

16:00 - 17:15
Symbolic ExecutionTechnical Papers at Bren 1414
Chair(s): Gordon Fraser University of Sheffield
16:00
25m
Talk
Accelerating Array Constraints in Symbolic Execution
Technical Papers
David Mitchel Perry Purdue University, Andrea Mattavelli Imperial College London, Xiangyu Zhang Purdue University, Cristian Cadar Imperial College London
DOI
16:25
25m
Talk
Improving the Cost-Effectiveness of Symbolic Testing Techniques for Transport Protocol Implementations under Packet Dynamics
Technical Papers
Wei Sun University of Nebraska-Lincoln, USA, Lisong Xu University of Nebraska-Lincoln, USA, Sebastian Elbaum University of Nebraska-Lincoln, USA
DOI
16:50
25m
Talk
Combining Symbolic Execution and Search-Based Testing for Programs with Complex Heap Inputs
Technical Papers
Pietro Braione University of Milano-Bicocca, Italy, Giovanni Denaro University of Milano-Bicocca, Italy, Andrea Mattavelli Imperial College London, Mauro Pezzè University of Milano-Bicocca, Italy
DOI