The STIC AmSud MISMT project is a collaborative project between teams at

  • Facultad de Matemática, Astronomía y Física (FaMAF), Universidad Nacional de Córdoba (UNC), Córdoba, Argentina
  • Departamento de Informática e Matemática Aplicada (DIMAp), Universidade Federal do Rio Grande do Norte (UFRN), Natal, Brazil
  • INRIA Nancy – Grand-Est, Loria, Nancy, France

Satisfiability Modulo Theories solving aims at building tools to automatically check the satisfiability of large logic formulas with interpreted and non-interpreted symbols. It has many applications but it is currently mostly used for verification of hardware and software. Modal logics are languages that have surprisingly low complexity even though they are very expressive. Many modal logics (specially temporal logics) are also used in software and hardware verification and many tools have been developed for both satisfiability and model checking.

The project combines the experience of the research groups to investigate SMT reasoning for modal logics, and ways to improve SMT reasoning in general via techniques inspired by modal reasoning. The French research group specializes on SMT reasoning, the Argentinean research group on computational modal logic.

In the past, the French and Argentinean teams have collaborated on research in modally inspired decidable fragments of first order logic. Currently, we are investigating the use of SMT techniques for satisfiability checking for different modal logics via translation. We also aim to use inspiration from modal logics (guards) to improve the handling of quantifiers in SMT. We are also investigating ways to take advantage of symmetry (both in the original modal formula and after translation) to improve automated deduction.


[15/09/14] Richard Bonichon and Claudia Tavares (Natal) are visiting the French team for two weeks

[01/09/14] Pablo Federico Dobal is starting a PhD thesis in Nancy.

[30/06/2014 - 04/07/2014] MISMT STIC AmSud Workshop in Nancy. Participants: Carlos Areces, Haniel Barbosa, David Déharbe, Pablo Federico Dobal Raul Fervari, Pascal Fontaine, Guillaume Hoffmann, Stephan Merz

[06/2014] Carlos Areces, Raul Fervari, and Guillaume Hoffmann (Cordoba) are visiting the French team for one month

[02/2014] Stephan Merz is visiting the Argentinean team for one month

[01/12/13] Haniel Barbosa is starting a PhD with a CORDI grant, under joint supervision with Natal and Nancy. Haniel will spend 9 months in Nancy and 3 months in Natal each year

[15/11/13] The STIC AmSud project MISMT has been accepted

[01/08/13] David Déharbe is coming for a sabbatical in Nancy for one year