Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively

Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

Modern verification tools frequently rely on compiling high-level specifications to SMT queries. However, the high-level specification language is usually more expressive than the available solvers and therefore some syntactically valid specifications must be rejected by the tool. In such cases, the challenge is to provide a comprehensible error message to the user that relates the original syntactic form of the specification to the semantic reason it has been rejected. In this paper we demonstrate how this analysis may be performed by combining a standard unification-based type-checker with type classes and automatic generalisation. Concretely, type-checking is used as a constructive procedure for under-approximating whether a given specification lies in the subset of problems supported by the solver. Any resulting proof of rejection can be transformed into a detailed explanation to the user. The approach is compositional and does not require the user to add extra typing annotations to their program. We subsequently describe how the type system may be leveraged to provide a sound and complete compilation procedure from suitably typed expressions to SMT queries, which we have verified in Agda.

Original languageEnglish
Title of host publicationCPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
EditorsRobbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic
PublisherAssociation for Computing Machinery
Pages102-120
Number of pages19
ISBN (Electronic)9798400700262
DOIs
Publication statusPublished - 11 Jan 2023
Event12th ACM SIGPLAN International Conference on Certified Programs and Proofs - Co-located with POPL 2023 - Boston, United States
Duration: 16 Jan 202317 Jan 2023

Conference

Conference12th ACM SIGPLAN International Conference on Certified Programs and Proofs - Co-located with POPL 2023
Abbreviated titleCPP 2023
Country/TerritoryUnited States
CityBoston
Period16/01/2317/01/23

Keywords

  • Agda
  • compilers
  • domain specific languages
  • SMT solvers
  • type-checking
  • verification

ASJC Scopus subject areas

  • Computer Science Applications

Fingerprint

Dive into the research topics of 'Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively'. Together they form a unique fingerprint.

Cite this