Christophe Ringeissen

logo inria

LORIA --- INRIA Nancy-Grand Est
615, rue du Jardin Botanique
BP 101, 54602 Villers-les-Nancy Cedex, France
Tel: (+33/0) 3 83 59 30 53
Fax: (+33/0) 3 83 27 83 19
Office: A 203

E-mail: Christophe . Ringeissen at loria . fr

Researcher at INRIA

CASSIS project, INRIA-Nancy Grand Est/LORIA


Research interests - keywords

Automated Deduction (Rewriting Techniques)
Constraint Programming (Constraint Archive)
Combination Methods in Automated Reasoning
Rewriting Logic, Algebraic Specifications


Events

IJCAR 2016 8th International Joint Conference on Automated Reasoning (Coimbra, Portugal, June 27 - July 2, 2016)

WRLA 2016 11th International Workshop on Rewriting Logic and its Applications (Eindhoven, The Netherlands, 2-3 April, 2016). An ETAPS 2016 satellite event

FroCoS'2015 10th International Symposium on Frontiers of Combining Systems (Wroclaw, Poland, 19-24 September, 2015)

CADE-25 25th International Conference on Automated Deduction (Berlin, Germany, 1-7 August, 2015)

UNIF'2015 29th International Workshop on Unification (Warsaw, Poland, June 28, 2015)

UNIF'2014 28th International Workshop on Unification (Vienna, Austria, July 13, 2014). Proceedings: html pdf

FroCoS'2013 9th International Symposium on Frontiers of Combining Systems (Nancy, France, 18-20 September, 2013)

CADE-24 24th International Conference on Automated Deduction (Lake Placid, USA, 9-14 June, 2013)

IWS 2012 2nd Joint International Workshop on Strategies in Rewriting, Proving and Programming (Workshop of IJCAR 2012)

AREIS 2012 Automated Reasoning for Enterprise Information Systems (Workshop of IJCAR 2012)

FroCoS'2011 8th International Workshop on Frontiers of Combining Systems (Saarbruecken, Germany)

IJCAR 2010 5th International Joint Conference on Automated Reasoning (Edinburgh, UK)

FroCoS'2009 7th International Workshop on Frontiers of Combining Systems (Trento, Italy)

IJCAR 2008 4th International Joint Conference on Automated Reasoning (Sidney, Australia)

FroCoS'2007 6th International Workshop on Frontiers of Combining Systems (Liverpool, UK)

Calculemus'06 13th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning

FroCoS'2005 5th International Workshop on Frontiers of Combining Systems (Vienna, Austria)

Special Issue of I&C on Combining Logical Systems (Deadline: January 22, 2005)

RULE'04 Rule-based Programming (Workshop of RDP'04)

PDPAR'03 Pragmatics of Decision Procedures in Automated Reasoning (Workshop of CADE-19)

UNIF'2002 16th International Workshop on Unification (Copenhagen, Denmark)

AMAST'2002 9th International Conference on Algebraic Methodology And Software Technology (Saint Gilles les Bains, Ile de la Réunion)

FroCoS'2002 4th International Workshop on Frontiers of Combining Systems (Santa Margherita Ligure, Italy)

STRATEGIES'2001 4th International Workshop on Strategies in Automated Deduction, held in conjunction with IJCAR'2001

ETAPS'2001 tutorial Rule-based programming using ELAN

FroCoS'2000 3rd International Workshop on Frontiers of Combining Systems (Nancy, France)


Projects

Bananas, Inria associate team (2012---2014)

Decert, ANR (2009---2012)

Vanaweb, Inria associate team (2008---2010)


Publications

For recent publications (starting from 2013), see here

Articles
Conferences
Proceedings


Theses

Combinaison de résolutions de contraintes (Combination of Constraint Solvers, french version). PhD thesis defended on December 21th, 1993. Also available here.

Raisonnement équationnel et méthodes de combinaison: de la programmation à la preuve (Equational Reasoning and Combination Methods: from Programs to Proofs, english version/french version). Habilitation thesis defended on November 27, 2009. Also available here.




Teaching

Decision Procedures and Verification of Programs, Master Recherche Informatique, LMFI, Université de Lorraine, 2015/16. Taught initially with Silvio Ranise. In 2015, taught with the collaboration of Carlos Castro and Pascal Fontaine.

  1. Introduction
  2. Decision Procedures for the theory of Equality
  3. Linear Arithmetic: basic techniques and the Simplex method
  4. Combining Decision Procedures
  5. Building Decision Procedures for Data Structures
  6. Boolean Solving
  7. Integrating Decision Procedures with Boolean Solving
  8. Applications: the veriT SMT solver