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

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

Matthew Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi · CPP · 2023 · machine-learning-verification · PDF · DOI · pldb

Cite

Cite as @daggitt-2023-compiling (helia, typst) · \cite{daggitt-2023-compiling} (LaTeX)

BibTeX

bibtex · 1 line

@inproceedings{daggitt-2023-compiling, series={CPP ’23}, title={Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively}, url={http://dx.doi.org/10.1145/3573105.3575674}, DOI={10.1145/3573105.3575674}, booktitle={Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs}, publisher={ACM}, author={Daggitt, Matthew L. and Atkey, Robert and Kokke, Wen and Komendantskaya, Ekaterina and Arnaboldi, Luca}, year={2023}, month=Jan, pages={102–120}, collection={CPP ’23} }

hayagriva YAML (typst)

yaml · 21 lines

daggitt-2023-compiling:
  type: article
  title: 'Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively'
  author:
  - Daggitt, Matthew L.
  - Atkey, Robert
  - Kokke, Wen
  - Komendantskaya, Ekaterina
  - Arnaboldi, Luca
  date: 2023-01
  page-range: 102-120
  url: http://dx.doi.org/10.1145/3573105.3575674
  serial-number:
    doi: 10.1145/3573105.3575674
  parent:
    type: proceedings
    title: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
    publisher: ACM
    parent:
      type: proceedings
      title: CPP ’23

Download: daggitt-2023-compiling.bib · daggitt-2023-compiling.yml

Cites 29 works (0 here)

External (29)

cvc5: A Versatile and Industrial-Strength SMT Solver (2022)
Strongly-Normalizing Higher-Order Relational Queries (2022)
Vehicle (software repository) (2022)
The Marabou Framework for Verification and Analysis of Deep Neural Networks (2019)
Semantic-based Automated Reasoning for AWS Access Policies using SMT (2018)
UCLID5: Integrating Modeling, Verification, Synthesis and Learning (2018)
Efficient neural network robustness certification with general activation functions (2018)
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (2017)
Dependent types and multi-monadic effects in F* (2016)
Liquid Haskell: Haskell as a theorem prover (2016)
Studies in Logic and the Foundations of Mathematics (2014)
CBMC – C Bounded Model Checker (2014)
Idris, a general-purpose dependently typed programming language: Design and implementation (2013)
The Script-Writer’s Dream: How to Write Great SQL in Your Own Language, and Be Sure It Will Succeed (2009)
Dependently Typed Programming in Agda (2009)
Z3: An Efficient SMT Solver (2008)
Program synthesis by sketching (2008)
Finite Instantiations for Integer Difference Logic (2006)
Cryptol: high assurance, retargetable crypto development and validation (2004)
An inverse of the evaluation functional for typed lambda -calculus (2002)
Types and programming languages (2002)
Monadic Presentations of Lambda Terms Using Generalized Inductive Types (1999)
de Bruijn notation as a nested datatype (1999)
An algorithm for type-checking dependent types (1996)
Substitution: A formal methods case study using monads and transformations (1994)
Functional unification of higher-order patterns (1993)
Kripke-style models for typed lambda calculus (1991)
Notions of computation and monads (1991)
How to make ad-hoc polymorphism less ad hoc (1989)