Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 15:21 - 15:43 at Sala II - Time Chair(s): Andrew C. Myers

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 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

15:21 - 16:49: TimeResearch Papers at Sala II
Chair(s): Andrew C. MyersCornell University
15:21 - 15:43
Type-Guided Worst-Case Input Generation
Research Papers
Di WangCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
Link to publication DOI Pre-print Media Attached File Attached
15:43 - 16:05
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Research Papers
Conrad WattUniversity of Cambridge, John RennerUniversity of California, San Diego, Natalie PopescuUniversity of California San Diego, Sunjay CauligiUCSD, Deian StefanUniversity of California San Diego
Link to publication DOI Media Attached File Attached
16:05 - 16:27
Modular Quantitative Monitoring
Research Papers
Rajeev AlurUniversity of Pennsylvania, Konstantinos MamourasUniversity of Pennsylvania, Caleb StanfordUniversity of Pennsylvania
Link to publication DOI Media Attached File Attached
16:27 - 16:49
CSS Minification via Constraint SolvingTOPLAS
Research Papers
Matthew HagueRoyal Holloway, University of London, Anthony Widjaja LinOxford University, Chih-Duo HongUniversity of Oxford
Media Attached File Attached