Scalable and Precise Refinement Types for Imperative Languages

Reviewed Paper In Proceedings

Author(s):Florian Lanzinger, Joshua Bachmeier, Mattias Ulbrich, and Werner Dietl
In:iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings
Publisher:Springer Nature Switzerland
Series:Lecture Notes in Computer Science
Volume:14300
Year:2023
Pages:377-383
PDF:
DOI:10.1007/978-3-031-47705-8_20

Abstract

In formal verification, there is a dichotomy between tools which are scalable and easy to use but imprecise, like most pluggable type systems, and tools which are expressive and precise but badly scalable and difficult to use, like deductive verification. Our previous research to create a formal link between refinement types and deductive verification allows programmers to use a scalable type system for most of the program, while automatically generating specifications for a deductive verifier for the difficult-to-prove parts. However, this is currently limited to immutable objects. In this work, we thus present an approach which combines uniqueness and refinement type systems in an imperative language. Unlike existing similar approaches, which limit refinements such that they cannot contain any reference-typed program variables, our approach allows more general refinements, because even if a type constraint is not provable in the type system itself, it can be translated and proven by a deductive verifier.

BibTeX

@InProceedings{LanzingerBachmeierUlbrichDietl2023,
  author    = {Florian Lanzinger and Joshua Bachmeier and Mattias Ulbrich and Werner Dietl},
  editor    = {Paula Herber and Anton Wijs},
  title     = {Scalable and Precise Refinement Types for Imperative Languages},
  booktitle = {iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands,
               November 13-15, 2023, Proceedings},
  year      = {2023},
  month     = nov,
  publisher = {Springer Nature Switzerland},
  address   = {Cham},
  series    = {Lecture Notes in Computer Science},
  volume    = {14300},
  pages     = {377--383},
  abstract  = {In formal verification, there is a dichotomy between tools which are scalable and easy to use
               but imprecise, like most pluggable type systems, and tools which are expressive and precise
               but badly scalable and difficult to use, like deductive verification.
               Our previous research to create a formal link between refinement types and deductive
               verification allows programmers to use a scalable type system for most of the program, while
               automatically generating specifications for a deductive verifier for the difficult-to-prove parts.
               However, this is currently limited to immutable objects.
               In this work, we thus present an approach which combines uniqueness and refinement type systems
               in an imperative language.
               Unlike existing similar approaches, which limit refinements such that they cannot contain any
               reference-typed program variables, our approach allows more general refinements, because even
               if a type constraint is not provable in the type system itself, it can be translated and proven
               by a deductive verifier.},
  isbn      = {978-3-031-47705-8},
  doi       = {10.1007/978-3-031-47705-8_20},
  pdf       = {PDF:/lanzinger/pdf/iFM2023PhDSymposium.pdf}
}