Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively
Modern verification tools frequently rely on compiling high-level specifications to SMT queries. However, usually the high-level specification language is 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 type-checker based on unification 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. Crucially, the approach 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.
Tue 17 JanDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30
|Terms for Efficient Proof Checking and ParsingRecorded Presentation|
Michael Färber Universität Innsbruck, Austria
|Compositional pre-processing for automated reasoning in dependent type theoryremote presentation|
Valentin Blot LMF, Inria, Université Paris-Saclay, Denis Cousineau Mitsubishi Electric R&D Centre Europe, Enzo Crance Mitsubishi Electric R&D Centre Europe, Louise Dubois de Prisque LMF, Inria, Université Paris-Saclay, Chantal Keller LRI, Université Paris-Sud, Assia Mahboubi INRIA, Pierre Vial Inria
|Practical and sound equality tests, automatically|
|Compiling higher-order specifications to SMT solvers: how to deal with rejection constructivelyremote presentation|