Matryoshka SIGNED
Fast Interactive Verification through Strong Higher-Order Automation
Total Cost €
0EC-Contrib. €
0Partnership
0Views
0Matryoshka project word cloud
Explore the words cloud of the Matryoshka project. It provides you a very rough idea of what is the project "Matryoshka" about.
Project "Matryoshka" data sheet
The following table provides information about the project.
| Coordinator |
STICHTING VU
Organization address contact info |
| Coordinator Country | Netherlands [NL] |
| Project website | http://matryoshka.gforge.inria.fr |
| Total cost | 1˙498˙438 € |
| EC max contribution | 1˙498˙438 € (100%) |
| Programme |
1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC)) |
| Code Call | ERC-2016-STG |
| Funding Scheme | ERC-STG |
| Starting year | 2017 |
| Duration (year-month-day) | from 2017-03-01 to 2022-02-28 |
Partnership
Take a look of project's partnership.
| # | ||||
|---|---|---|---|---|
| 1 | STICHTING VU | NL (AMSTERDAM) | coordinator | 994˙688.00 |
| 2 | INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE | FR (LE CHESNAY CEDEX) | participant | 503˙750.00 |
Map
Project objective
Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. The situation has improved with the integration of first-order automatic theorem provers -- superposition provers and SMT (satisfiability modulo theories) solvers -- through middleware such as Sledgehammer for Isabelle, codeveloped by the PI; but this research has now reached the point of diminishing returns. Only so much can be done when viewing automatic provers as black boxes.
To make interactive verification more cost-effective, we propose to deliver very high levels of automation to users of proof assistants by fusing and extending two lines of research: automatic and interactive theorem proving. This is our grand challenge. Our starting point is that first-order automatic provers are the best tools available for performing most of the logical work. Our approach will be to enrich superposition and SMT with higher-order reasoning in a careful manner, to preserve their desirable properties. We will design proof rules and strategies, guided by representative benchmarks from interactive verification.
With higher-order superposition and higher-order SMT in place, we will develop highly automatic provers building on modern superposition provers and SMT solvers, following a novel stratified architecture. To reach end users, these new provers will be integrated in proof assistants, including Coq, Isabelle, and the TLA Proof System, and will be available as backends to more specialized verification tools. The users of proof assistants and similar tools stand to experience substantial productivity gains: In the past five years, the success rate of automatic provers on interactive proof obligations from a representative benchmark suite has risen from 47% to 77%; with this project, we aim at 90%--95% proof automation.
Publications
| year | authors and title | journal | last update |
|---|---|---|---|
| 2020 |
Paula Chocron, Pascal Fontaine, Christophe Ringeissen Politeness and Combination Methods for Theories with Bridging Functions published pages: 97-134, ISSN: 0168-7433, DOI: 10.1007/s10817-019-09512-4 |
Journal of Automated Reasoning 64/1 | 2020-04-01 |
| 2019 |
Mathias Fleury, Hans-Jörg Schurr Reconstructing veriT Proofs in Isabelle/HOL published pages: 36-50, ISSN: 2075-2180, DOI: 10.4204/EPTCS.301.6 |
Electronic Proceedings in Theoretical Computer Science 301 | 2020-04-01 |
| 2020 |
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine Scalable Fine-Grained Proofs for Formula Processing published pages: 485-510, ISSN: 0168-7433, DOI: 10.1007/s10817-018-09502-y |
Journal of Automated Reasoning 64/3 | 2020-04-01 |
| 2019 |
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow A Formal Proof of the Expressiveness of Deep Learning published pages: 347-368, ISSN: 0168-7433, DOI: 10.1007/s10817-018-9481-5 |
Journal of Automated Reasoning 63/2 | 2020-03-11 |
| 2018 |
Pascal Fontaine, Mizuhito Ogawa, Van Khanh To, Xuan Tung Vu Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT published pages: , ISSN: , DOI: |
SC-square 2018 - Third International Workshop on Satisfiability Checking and Symbolic Computation, Jul 2018, Oxford, United Kingdom | 2020-03-11 |
| 2019 |
Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel Bindings as bounded natural functors published pages: 1-34, ISSN: 2475-1421, DOI: 10.1145/3290335 |
Proceedings of the ACM on Programming Languages 3/POPL | 2020-03-11 |
| 2017 |
Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms published pages: 432-453, ISSN: , DOI: |
26th International Conference on Automated Deduction (CADE-26) | 2020-03-11 |
| 2017 |
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel Friends with benefits: Implementing corecursion in foundational proof assistants published pages: 111-140, ISSN: , DOI: |
26th European Symposium on Programming (ESOP 2017) | 2020-03-11 |
| 2017 |
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Tung Vu Subtropical satisfiability published pages: 189-206, ISSN: , DOI: |
11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) | 2020-03-11 |
| 2018 |
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality published pages: 333-365, ISSN: 0168-7433, DOI: 10.1007/s10817-018-9455-7 |
Journal of Automated Reasoning 61/1-4 | 2020-03-11 |
| 2017 |
Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand A lambda-free higher-order recursive path order published pages: 461-479, ISSN: , DOI: |
20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017) | 2020-03-11 |
| 2017 |
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine Language and proofs for higher-order SMT (work in progress) published pages: 15-22, ISSN: , DOI: |
5th Workshop on Proof eXchange for Theorem Proving (PxTP 2017) | 2020-03-11 |
| 2017 |
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Soundness and Completeness Proofs by Coinductive Methods published pages: 149-179, ISSN: 0168-7433, DOI: |
Journal of Automated Reasoning 58(1) | 2020-03-11 |
| 2017 |
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds Congruence closure with free variables published pages: 214-230, ISSN: , DOI: |
23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Part II | 2020-03-11 |
| 2017 |
Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow A Formal Proof of the Expressiveness of Deep Learning published pages: 46-64, ISSN: , DOI: |
8th Conference on Interactive Theorem Proving (ITP 2017) | 2020-03-11 |
| 2018 |
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, Uwe Waldmann Superposition for Lambda-Free Higher-Order Logic published pages: 28-46, ISSN: , DOI: 10.1007/978-3-319-94205-6_3 |
9th International Joint Conference on Automated Reasoning (IJCAR 2018) | 2020-03-11 |
| 2017 |
Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine Scalable Fine-Grained Proofs for Formula Processing published pages: 398-412, ISSN: , DOI: |
26th International Conference on Automated Deduction (CADE-26) | 2020-03-11 |
| 2017 |
Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, OndÅ™ej KunÄar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic published pages: 3-21, ISSN: , DOI: |
11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) | 2020-03-11 |
| 2017 |
Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel Foundational Nonuniform (Co)datatypes for Higher-Order Logic published pages: 1-12, ISSN: , DOI: |
32nd Annual IEEE Symposium on Logic in Computer Science (LICS 2017) | 2020-03-11 |
| 2018 |
Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann Formalizing Bachmair and Ganzinger\'s ordered resolution prover published pages: 89-107, ISSN: , DOI: 10.1007/978-3-319-94205-6_7 |
9th International Joint Conference on Automated Reasoning (IJCAR 2018) | 2020-03-11 |
| 2017 |
Jeremy Avigad, Johannes Hölzl, Luke Serafin A Formally Verified Proof of the Central Limit Theorem published pages: 389-423, ISSN: 0168-7433, DOI: |
Journal of Automated Reasoning 59(4) | 2020-03-11 |
| 2017 |
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL published pages: , ISSN: , DOI: |
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) | 2020-03-11 |
| 2017 |
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality published pages: 4786-4790, ISSN: , DOI: |
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence | 2020-03-11 |
| 2017 |
Andrew Reynolds, Jasmin Christian Blanchette A Decision Procedure for (Co)datatypes in SMT Solvers published pages: 341-362, ISSN: 0168-7433, DOI: |
Journal of Automated Reasoning 58(3) | 2020-03-11 |
| 2018 |
Andrew Reynolds, Haniel Barbosa, Pascal Fontaine Revisiting Enumerative Instantiation published pages: 112-131, ISSN: , DOI: 10.1007/978-3-319-89963-3_7 |
24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018) | 2020-03-11 |
| 2017 |
Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann Towards Strong Higher-Order Automation for Fast Interactive Verification published pages: 16-7, ISSN: , DOI: 10.29007/3ngx |
EPiC Series in Computing volume 51 | 2020-03-11 |
| 2017 |
Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo NP-completeness of small conflict set generation for congruence closure published pages: 533-544, ISSN: 0925-9856, DOI: |
Formal Methods in System Design 51(3) | 2020-03-11 |
| 2018 |
Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard Superposition with Datatypes and Codatatypes published pages: 370-387, ISSN: , DOI: 10.1007/978-3-319-94205-6_25 |
9th International Joint Conference on Automated Reasoning (IJCAR 2018) | 2020-03-11 |
Are you the coordinator (or a participant) of this project? Plaese send me more information about the "MATRYOSHKA" project.
For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.
Send me an email (fabio@fabiodisconzi.com) and I put them in your project's page as son as possible.
Thanks. And then put a link of this page into your project's website.
The information about "MATRYOSHKA" are provided by the European Opendata Portal: CORDIS opendata.