Read on Twitter
We’re currently running a seminar on specification & testing where we ask the student to write one or two short summaries on selected papers, every week. I thought I’d take the challenge to write summaries fitting into one tweet.
So here’s my summary for our first paper.
So here’s my summary for our first paper.
Summary https://dl.acm.org/doi/10.1145/351240.351266. Approach for checking properties of small code units w/ random inputs. Adapted for many PLs. Properties can have preconditions (danger: vacuous satisfaction). Writing custom generators necessary for own types. Limitation: How to measure coverage?
Appendix.
1) The coverage problem reminds me of paper by @vardi et al. https://link.springer.com/chapter/10.1007%2F978-3-540-39724-3_11 on coverage metrics for formal verification. Did somebody implement this for QuickCheck-like approaches?
1) The coverage problem reminds me of paper by @vardi et al. https://link.springer.com/chapter/10.1007%2F978-3-540-39724-3_11 on coverage metrics for formal verification. Did somebody implement this for QuickCheck-like approaches?
2) Generator transformation reminds me of the Zest approach to semantic fuzzing by @moarbugs, @cestlemieux, @koushik77 et al. https://dl.acm.org/doi/10.1145/3293882.3330576: Different int lists give rise to different generator transformers.
3) Errors discovered due to either generators, specification, or program. @GuillaumePetiot et al. https://link.springer.com/chapter/10.1007%2F978-3-319-41135-4_8 use testing to attribute failed proof attempts to roughly these classes.
4) There are by now a lot of papers addressing problem of creating custom generators (not only difficult, but also soundness-critical!). E.g., https://dl.acm.org/doi/10.1145/3093333.3009868 & https://link.springer.com/chapter/10.1007%2F978-3-030-31157-5_12, which we’ll also discuss in the seminar.
5) Here’s a list of QuickCheck implementations for different programming languages: https://hypothesis.works/articles/quickcheck-in-every-language/
