Coverage Types for Resource-Based Policies
Angelo Passarelli, Gian-Luigi Ferrari

TL;DR
This paper introduces an extension to Coverage Types that incorporates resource effect annotations, enabling static verification of resource usage correctness in property-based testing frameworks.
Contribution
It extends Coverage Types with effect annotations to verify resource policies, ensuring test generator correctness regarding resource consumption.
Findings
Successfully integrates resource effects into Coverage Types
Enables static verification of resource usage policies
Supports correctness guarantees in property-based testing
Abstract
Coverage Types provide a suitable type mechanism that integrates under-approximation logic to support Property-Based Testing. They are used to type the return value of a function that represents an input test generator. This allows us to statically assert that an input test generator not only produces valid input tests but also generates all possible ones, ensuring completeness. In this paper, we extend the coverage framework to guarantee the correctness of Property-Based Testing with respect to resource usage in the input test generator. This is achieved by incorporating into Coverage Types a notion of effect, which represents an over-approximation of operations on relevant resources. Programmers can define resource usage policies through logical annotations, which are then verified against the effect associated with the Coverage Type.
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.
Taxonomy
TopicsClimate Change Policy and Economics
