Tue 25 Jun 2019 08:30 - 08:50 at 229AB - Bug Finding & Testing I Chair(s): Cindy Rubio-González

We present counterfactual symbolic execution, a new approach that produces counterexamples that localize the causes of failure of static verification.

First, we develop a notion of symbolic weak head normal form and use it to define lazy symbolic execution reduction rules for non-strict languages like Haskell. Second, we introduce counterfactual branching, a new method to identify places where verification fails due to imprecise specifications (as opposed to incorrect code). Third, we show how to use counterfactual symbolic execution to localize refinement type errors, by translating refinement types into assertions. We implement our approach in a new Haskell symbolic execution engine, G2, and evaluate it on a corpus of 7550 errors gathered from users of the LiquidHaskell refinement type system. We show that for 97.7% of these errors, G2 is able to quickly find counterexamples that show how the code or specifications must be fixed to enable verification.

Conference Day
Tue 25 Jun

Displayed time zone: Tijuana, Baja California change

08:30 - 09:30
Bug Finding & Testing IPLDI Research Papers at 229AB
Chair(s): Cindy Rubio-GonzálezUniversity of California, Davis
08:30
20m
Talk
Lazy Counterfactual Symbolic Execution
PLDI Research Papers
William T. HallahanYale University, Anton XueYale University, Maxwell Troy BlandUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California, San Diego, Ruzica PiskacYale University, USA
Media Attached
08:50
20m
Talk
Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript
PLDI Research Papers
Blake Loring, Duncan MitchellRoyal Holloway, University of London, Johannes KinderBundeswehr University Munich
Media Attached
09:10
20m
Talk
Effective Floating-Point Analysis via Weak-Distance Minimization
PLDI Research Papers
Zhoulai FuIT University of Copenhagen, Denmark, Zhendong SuETH Zurich