[Matryoshka-devel] News

Pascal Fontaine Pascal.Fontaine at loria.fr
Wed Jul 12 11:01:14 CEST 2017

Dear Matryoshka Friends,

I have a few good news to share from Nancy.

First, we are very happy to announce that Daniel El Ouraoui, a master 
student from MPRI (Master Parisien de Recherche en Informatique, the 
main research CS master in Paris) and currently doing an internship with 
Matryoshka on higher-order SMT, is joining Matryoshka as a PhD student, 
starting October 2017! Jasmin and myself will be co-advisors.

Second, a few Matryoshka-related works have been accepted and will be 
presented during this summer (they are available in some form on the 
Matryoshka web site):

   Scalable fine-grained proofs for formula processing
   Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine.

Accepted at CADE 2017 (Gothenburg), and also as presentation only at 
PxTP 2017 (Brasilia).  This will be presented by Haniel.

   Subtropical satisfiability
   Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, and Xuan Tung Vu

Accepted at FroCoS 2017 (Brasilia), and also as presentation only at SC² 
2017 (Kaiserslautern) and SMT 2017 (Heidelberg).  I will present this.

   Congruence closure with free variables
   Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds.

We already announced the presentation of this at TACAS 2017.  It is also 
accepted as presentation only at SMT 2017 (Heidelberg) and as a poster 
at FroCoS 2017 (Brasilia).  This will be presented by Haniel.

There will be two Matryoshka-related talks at the ARCADE workshop 2017 

   Towards Strong Higher-Order Automation for Fast Interactive Verification
   Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz and Uwe 

   Making Automatic Theorem Provers more Versatile
   Simon Cruanes

And we are already making some progress on higher-order SMT!

   Language and proofs for Higher-order SMT (work in progress)
   Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El 
Ouraoui and Pascal Fontaine

is accepted at PxTP 2017 (Brasilia).  It is not decided yet who will 
present but four authors will be in Brasilia.

As you can infer from above, many people from Nancy will travel the next 

SMT workshop: Haniel, Thomas, Pascal

SC² workshop: Haniel, Thomas, Pascal

VTSA+SC² summer schools: Haniel, Hans-Jörg, Daniel, Thomas, Pascal

ARCADE+CADE: Haniel, Simon, Pascal

FroCoS: Haniel, Simon, Pascal

We hope to meet you at one of these events soon!



More information about the matryoshka-devel mailing list