Methods for Higher-Order reasoning in SMT
Méthodes pour le raisonnement d'ordre supérieur dans SMT
Résumé
Many applications, notably in the context of verification (for critical systems in transportation, energy, etc.), rely on checking the satisfiability of logic formulas. Satisfiability-modulo-theories (SMT) solvers handle large formulas in expressive languages with built-in and custom operators (e.g. arithmetic and data structure operators). These tools are built using a cooperation of a SAT (propositional satisfiability) solver to handle the Boolean structure of the formula and theory reasoners to tackle the atomic formulas (e.g. « x > y+z » for the theory of arithmetic). Currently, SMT solvers only handle first-order logic. They cannot reason about higher-order expressions, and they generally cannot perform proofs by induction. This is unfortunate, because most interactive verification tools, which use SMT solvers as back-end reasoning engines, offer higher-order languages. This thesis offers solutions to improve interactions between automatic solvers and proof assistants. In particular, we answer two important issues allowing us to improve the use of SMT solvers within proof assistants. Our first contribution consists in providing a suitable architecture to SMT solvers for higher-order logic. The second contribution aims to improve quantifier reasoning inside SMT solvers. For both approaches, we developed a practical implementation and provide a concrete evaluation on a large collection of problems mostly coming from formalization problems. The results obtained during these evaluations are encouraging and show that the developed techniques can provide good improvements for SMT solvers.Many applications, notably in the context of verification (for critical systems in transportation, energy, etc.), rely on checking the satisfiability of logic formulas. Satisfiability-modulo-theories (SMT) solvers handle large formulas in expressive languages with built-in and custom operators (e.g. arithmetic and data structure operators). These tools are built using a cooperation of a SAT (propositional satisfiability) solver to handle the Boolean structure of the formula and theory reasoners to tackle the atomic formulas (e.g. « x > y+z » for the theory of arithmetic). Currently, SMT solvers only handle first-order logic. They cannot reason about higher-order expressions, and they generally cannot perform proofs by induction. This is unfortunate, because most interactive verification tools, which use SMT solvers as back-end reasoning engines, offer higher-order languages. This thesis offers solutions to improve interactions between automatic solvers and proof assistants. In particular, we answer two important issues allowing us to improve the use of SMT solvers within proof assistants. Our first contribution consists in providing a suitable architecture to SMT solvers for higher-order logic. The second contribution aims to improve quantifier reasoning inside SMT solvers. For both approaches, we developed a practical implementation and provide a concrete evaluation on a large collection of problems mostly coming from formalization problems. The results obtained during these evaluations are encouraging and show that the developed techniques can provide good improvements for SMT solvers.
La vérification formelle de programmes informatiques ou de systèmes dits critiques tels que dans le transport, l'énergie, etc, est essentielle pour garantir le bon fonctionnement de ces systèmes. Les méthodes de vérification employées s'appuient très fortement sur des procédés mathématiques et logiques permettant de raisonner de manière formelle sur le comportement de ces systèmes. Ces procédés définissent généralement les comportements sous forme de grands ensembles de contraintes logiques. L'approche par satisfaisabilité est une méthode largement utilisée pour vérifier ces contraintes et est un exemple de cas, où les solveurs SMT (satisfaisabilité modulo théories) sont fortement sollicités. Généralement, les solveurs SMT ne gèrent que la logique de premier ordre. Ils ne peuvent pas raisonner sur des expressions d'ordre supérieur, et ils ne peuvent généralement pas effectuer de preuves par induction. C'est regrettable, car la plupart des outils de vérification interactifs, qui utilisent les solveurs SMT, utilisent des langages d'ordre supérieur. L'objectif de cette thèse dans sa globalité est d'offrir des solutions pour améliorer les interactions entre solveur automatique et assistant de preuves. En particulier nous répondons à deux problématiques importantes permettant d'améliorer les usages de solveurs SMT au sein des assistants de preuves. Notre première contribution permet de réduire l'écart entre solveur et assistant de preuve en proposant une architecture adaptée pour la logique d'ordre supérieur. La seconde contribution permet d'améliorer les capacités de raisonnement des solveurs SMT pour les quantificateurs. Pour les deux approches développées nous apportons un ensemble d'évaluation sur des problèmes extraits pour la grande majorité de problèmes de formalisation. Les résultats obtenus lors de ces évaluations sont encourageants et montrent que les techniques développées dans cette thèse peuvent apporter de bonnes améliorations pour les solveurs SMT. Ce doctorat s'est effectué dans le cadre du projet ERC de J. Blanchette (Matryoshka), un ambitieux projet quinquennal qui vise à construire des prouveurs automatiques utiles pour la vérification interactive, et réduire l'écart entre les prouveurs interactifs et solveurs automatiques. L'un des objectifs concrets du projet est d'étendre les capacités de raisonnement des solveurs SMT vers l'ordre supérieur.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|