This paper presents a novel technique for type-guided worst-case input generation for functional programs. The technique builds on automatic amortized resource analysis (AARA), a type-based technique for deriving symbolic bounds on the resource usage of functions. Worst-case input generation is performed by an algorithm that takes as input a function, its resource-annotated type derivation in AARA, and a skeleton that describes the shape and size of the input that is to be generated. If successful, the algorithm fills in integers, booleans, and data structures to produce a value of the shape given by the skeleton. The soundness theorem states that the generated value exhibits the highest cost among all arguments of the functions that have the shape of the skeleton. This cost corresponds exactly to the worst-case bound that is established by the type derivation. In this way, a successful completion of the algorithm proves that the bound is tight for inputs of the given shape. Correspondingly, a relative completeness theorem is proved to show that the algorithm succeeds if and only if the derived worst-case bound is tight. The theorem is relative because it depends on a decision procedure for constraint solving. The technical development is presented for a simple first-order language with linear resource bounds. However, the technique scales to and has been implemented for Resource Aware ML, an implementation of AARA for a fragment of OCaml with higher-order functions, user-defined data types, and types for polynomial bounds. Experiments demonstrate that the technique works effectively and can derive worst-case inputs with hundreds of integers for sorting algorithms, operations on search trees, and insertions into hash tables.
Slides (popl19.pdf) | 9.54MiB |
Thu 17 JanDisplayed time zone: Belfast change
15:21 - 16:49 | |||
15:21 22mTalk | Type-Guided Worst-Case Input Generation Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
15:43 22mTalk | CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem Research Papers Conrad Watt University of Cambridge, John Renner University of California, San Diego, Natalie Popescu University of California San Diego, Sunjay Cauligi UCSD, Deian Stefan University of California San Diego Link to publication DOI Media Attached File Attached | ||
16:05 22mTalk | Modular Quantitative Monitoring Research Papers Rajeev Alur University of Pennsylvania, Konstantinos Mamouras University of Pennsylvania, Caleb Stanford University of Pennsylvania Link to publication DOI Media Attached File Attached | ||
16:27 22mTalk | CSS Minification via Constraint SolvingTOPLAS Research Papers Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Chih-Duo Hong University of Oxford Media Attached File Attached |