Opendata, web and dolomites

Matryoshka SIGNED

Fast Interactive Verification through Strong Higher-Order Automation

Total Cost €

0

EC-Contrib. €

0

Partnership

0

Views

0

Project "Matryoshka" data sheet

The following table provides information about the project.

Coordinator
STICHTING VU 

Organization address
address: DE BOELELAAN 1105
city: AMSTERDAM
postcode: 1081 HV
website: www.vu.nl

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 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.

# participants  country  role  EC contrib. [€] 
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
List of publications.
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.

More projects from the same programme (H2020-EU.1.1.)

PROGRESS (2019)

The Enemy of the Good: Towards a Theory of Moral Progress

Read More  

FICOMOL (2019)

Field Control of Cold Molecular Collisions

Read More  

OBSERVE (2020)

Overcoming cellular barriers to therapeutic RNA delivery using extracellular vesicles

Read More