Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Authors: 
Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca ArnaboldiAuthors Info & Claims
Pages 102 - 120
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.
References
[1]
Thorsten Altenkirch and Bernhard Reus. 1999. Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In Computer Science Logic, 13th International Workshop, CSL ’99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, Jörg Flum and Mario Rodríguez-Artalejo (Eds.) (Lecture Notes in Computer Science, Vol. 1683). Springer, 453–468. https://doi.org/10.1007/3-540-48168-0_32
[2]
John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Luckow, Neha Rungta, Oksana Tkachuk, and Carsten Varming. 2018. Semantic-based automated reasoning for AWS access policies using SMT. In 2018 Formal Methods in Computer Aided Design (FMCAD). 1–9.
[3]
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, Dana Fisman and Grigore Rosu (Eds.) (Lecture Notes in Computer Science, Vol. 13243). Springer, 415–442. https://doi.org/10.1007/978-3-030-99524-9_24
[4]
Françoise Bellegarde and James Hook. 1994. Substitution: A Formal Methods Case Study Using Monads and Transformations. Sci. Comput. Program., 23, 2-3 (1994), 287–311. https://doi.org/10.1016/0167-6423(94)00022-0
[5]
Ulrich Berger and Helmut Schwichtenberg. 1991. An Inverse of the Evaluation Functional for Typed lambda-calculus. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS ’91), Amsterdam, The Netherlands, July 15-18, 1991. IEEE Computer Society, 203–211. https://doi.org/10.1109/LICS.1991.151645
[6]
Richard S. Bird and Ross Paterson. 1999. De Bruijn Notation as a Nested Datatype. J. Funct. Program., 9, 1 (1999), 77–91. https://doi.org/10.1017/s0956796899003366
[7]
Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of functional programming, 23, 5 (2013), 552–593.
[8]
Ezra Cooper. 2009. The Script-Writer’s Dream: How to Write Great SQL in Your Own Language, and Be Sure It Will Succeed. In Database Programming Languages - DBPL 2009, 12th International Symposium, Lyon, France, August 24, 2009. Proceedings, Philippa Gardner and Floris Geerts (Eds.) (Lecture Notes in Computer Science, Vol. 5708). Springer, 36–51. https://doi.org/10.1007/978-3-642-03793-1_3
[9]
Thierry Coquand. 1996. An algorithm for type-checking dependent types. Science of Computer Programming, 26, 1-3 (1996), 167–177.
[10]
Matthew L. Daggitt, Wen Kokke, Atkey Bob, Natalia Ślusarz, and Marco Casadio. 2022. Vehicle. https://github.com/vehicle-lang/vehicle Accessed on 22.09.2022
[11]
Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. 337–340.
[12]
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett. 2017. SMTCoq: A plug-in for integrating SMT solvers into Coq. In International Conference on Computer Aided Verification. 126–133.
[13]
Jean-Yves Girard. 1971. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination de coupures dans l’analyse et la théorie des types. In Studies in Logic and the Foundations of Mathematics. 63, Elsevier, 63–92.
[14]
Guy Katz, Derek A Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, and Aleksandar Zeljić. 2019. The Marabou framework for verification and analysis of deep neural networks. In International Conference on Computer Aided Verification. 443–452.
[15]
Hyondeuk Kim and Fabio Somenzi. 2006. Finite instantiations for integer difference logic. In 2006 Formal Methods in Computer Aided Design. 31–38.
[16]
Daniel Kroening and Michael Tautschnig. 2014. CBMC–C bounded model checker. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 389–391.
[17]
Jeffrey R Lewis and Brad Martin. 2003. Cryptol: High assurance, retargetable crypto development and validation. In IEEE Military Communications Conference, 2003. MILCOM 2003. 2, 820–825.
[18]
John C. Mitchell and Eugenio Moggi. 1991. Kripke-Style Models for Typed lambda Calculus. Ann. Pure Appl. Log., 51, 1-2 (1991), 99–124. https://doi.org/10.1016/0168-0072(91)90067-V
[19]
Eugenio Moggi. 1991. Notions of Computation and Monads. Inf. Comput., 93, 1 (1991), 55–92. https://doi.org/10.1016/0890-5401(91)90052-4
[20]
Tobias Nipkow. 1993. Functional unification of higher-order patterns. In [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science. 64–74.
[21]
Ulf Norell. 2008. Dependently typed programming in Agda. In International school on advanced functional programming. 230–266.
[22]
Benjamin C Pierce. 2002. Types and programming languages. MIT press.
[23]
Wilmer Ricciotti and James Cheney. 2022. Strongly-Normalizing Higher-Order Relational Queries. Log. Methods Comput. Sci., 18, 3 (2022), https://doi.org/10.46298/lmcs-18(3:23)2022
[24]
Sanjit A Seshia and Pramod Subramanyan. 2018. UCLID5: Integrating modeling, verification, synthesis and learning. In 2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). 1–10.
[25]
Armando Solar-Lezama. 2008. Program synthesis by sketching. University of California, Berkeley.
[26]
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, and Markulf Kohlweiss. 2016. Dependent types and multi-monadic effects in F. In Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 256–270.
[27]
Niki Vazou. 2016. Liquid Haskell: Haskell as a theorem prover. University of California, San Diego.
[28]
Philip Wadler and Stephen Blott. 1989. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 60–76.
[29]
Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems, 31 (2018).
Index Terms
- Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Recommendations
Compiling Modechart specifications
RTSS '95: Proceedings of the 16th IEEE Real-Time Systems SymposiumThe Modechart specification language is a formalism for the specification of real-time systems. A toolset for specification, analysis and simulation for Modechart specifications exists for supporting the design and construction of real-time systems. ...
Improved usability and performance of SMT solvers for debugging specifications
It is now common to construct an extended static checker or software verification system using an SMT theorem prover as the underlying logical verifier. SMT provers have improved significantly in performance over the last several years. However, their ...
A Decision Procedure for (Co)datatypes in SMT Solvers
We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2023
347 pages
ISBN:9798400700262
DOI:10.1145/3573105
- General Chairs:
- Robbert Krebbers,
- Dmitriy Traytel,
- Program Chairs:
- Brigitte Pientka,
- Steve Zdancewic
Copyright © 2023 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 11 January 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
CPP '23
Sponsor:
CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 16 - 17, 2023
MA, Boston, USA
Acceptance Rates
Overall Acceptance Rate 18 of 26 submissions, 69%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 123Total Downloads
- Downloads (Last 12 months)23
- Downloads (Last 6 weeks)4
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in