Beyond the elementary representations of program invariants over algebraic data types

Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

Abstract

First-order logic is a natural way of expressing properties of computation. It is traditionally used in various program logics for expressing the correctness properties and certificates. Although such representations are expressive for some theories, they fail to express many interesting properties of algebraic data types (ADTs). In this paper, we explore three different approaches to represent program invariants of ADT-manipulating programs: tree automata, and first-order formulas with or without size constraints. We compare the expressive power of these representations and prove the negative definability of both first-order representations using the pumping lemmas. We present an approach to automatically infer program invariants of ADT-manipulating programs by a reduction to a finite model finder. The implementation called RInGen has been evaluated against state-of-the-art invariant synthesizers and has been experimentally shown to be competitive. In particular, program invariants represented by automata are capable of expressing more complex properties of computation and their automatic construction is often less expensive.

Original languageEnglish
Title of host publicationPLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
EditorsStephen N. Freund, Eran Yahav
PublisherAssociation for Computing Machinery
Pages451-465
Number of pages15
ISBN (Electronic)9781450383912
DOIs
StatePublished - 18 Jun 2021
Event42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021 - Virtual, Online, Canada
Duration: 20 Jun 202125 Jun 2021

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021
Country/TerritoryCanada
CityVirtual, Online
Period20/06/2125/06/21

Scopus subject areas

  • Software

Keywords

  • algebraic data types
  • finite models
  • first-order definability
  • invariant representation
  • invariants
  • tree automata

Cite this