Scalable and Precise Refinement Types for Imperative Languages

@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}
}