Type Targeted Testing
Eric L. Seidel, Niki Vazou, Ranjit Jhala

TL;DR
Type targeted testing leverages refinement types and SMT solvers to generate comprehensive test suites from high-level specifications, enabling systematic testing and a pathway toward verification.
Contribution
This paper introduces a novel technique that converts refinement types into SMT queries for automated test generation, implemented in the TARGET tool.
Findings
TARGET effectively tests a wide range of properties.
The approach compares favorably with existing testing methods.
It provides a gradual transition from testing to verification.
Abstract
We present a new technique called type targeted testing, which translates precise refinement types into comprehensive test-suites. The key insight behind our approach is that through the lens of SMT solvers, refinement types can also be viewed as a high-level, declarative, test generation technique, wherein types are converted to SMT queries whose models can be decoded into concrete program inputs. Our approach enables the systematic and exhaustive testing of implementations from high-level declarative specifications, and furthermore, provides a gradual path from testing to full verification. We have implemented our approach as a Haskell testing tool called TARGET, and present an evaluation that shows how TARGET can be used to test a wide variety of properties and how it compares against state-of-the-art testing approaches.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
