Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Wed 20 Jan 2021 18:40 - 18:50 at POPL-A - Program Analysis

Refinement types enable lightweight verification of functional programs. Algorithms for statically inferring refinement types typically work by reduction to solving systems of constraint Horn clauses extracted from typing derivations. An example is Liquid type inference, which solves the extracted constraints using predicate abstraction. However, the reduction to constraint solving in itself already signifies an abstraction of the program semantics that affects the precision of the overall static analysis. To better understand this issue, we study the type inference problem in its entirety through the lens of abstract interpretation. We propose a new refinement type system that is parametric with the choice of the abstract domain of type refinements as well as the degree to which it tracks context-sensitive control flow information. We then derive an accompanying parametric inference algorithm as an abstract interpretation of a novel data flow semantics of functional programs. We further show that the type system is sound and complete with respect to the constructed abstract semantics. Our theoretical development reveals the key abstraction steps inherent in refinement type inference algorithms. The trade-off between precision and efficiency of these abstraction steps is controlled by the parameters of the type system. Existing refinement type systems and their respective inference algorithms, such as Liquid types, are captured by concrete parameter instantiations. We have implemented our framework in a prototype tool and evaluated it for a range of new parameter instantiations (e.g., using octagons and polyhedra for expressing type refinements). The tool compares favorably against other existing tools. Our evaluation indicates that our approach can be used to systematically construct new refinement type inference algorithms that are both robust and precise.

Wed 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30
Program AnalysisPOPL at POPL-A
18:30
10m
Talk
Verifying Correct Usage of Context-Free API Protocols
POPL
Kostas Ferles UT Austin, Jon Stephens University of Texas at Austin, Işıl Dillig University of Texas at Austin
Link to publication DOI
18:40
10m
Talk
Data Flow Refinement Type Inference
POPL
Zvonimir Pavlinovic Google, USA, Yusen Su New York University, University of Waterloo, Thomas Wies New York University, USA
Link to publication DOI
18:50
10m
Talk
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
POPL
Jay P. Lim Rutgers University, USA, Mridul Aanjaneya Rutgers University, John Gustafson National University of Singapore, Santosh Nagarakatte Rutgers University, USA
Link to publication DOI
19:00
10m
Talk
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow GraphsDistinguished Paper
POPL
Julian Rosemann Saarland University, Saarland Informatics Campus, Simon Moll NEC Deutschland, Sebastian Hack Saarland University, Germany
Link to publication DOI
19:10
10m
Talk
Relatively Complete Verification of Probabilistic Programs
POPL
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja ETH Zurich
Link to publication DOI
19:20
10m
Talk
A Practical Mode System for Recursive Definitions
POPL
Alban Reynaud ENS Lyon, Gabriel Scherer INRIA Saclay, Jeremy Yallop University of Cambridge
Link to publication DOI Pre-print