Lazy counterfactual symbolic execution
| Autor: | William T. Hallahan, Ranjit Jhala, Anton Xue, Maxwell Bland, Ruzica Piskac |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Counterfactual thinking
Reduction (recursion theory) Computer science Programming language 020207 software engineering 02 engineering and technology Type (model theory) computer.software_genre Symbolic execution Branching (linguistics) 020204 information systems 0202 electrical engineering electronic engineering information engineering Code (cryptography) Haskell computer computer.programming_language Counterexample |
| Zdroj: | PLDI |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|