-
A Decision Procedure for a Fragment of Set Theory Involving Monotone, Additiv...
2LS is a decidable many-sorted set-theoretic language involving one sort for elements and one sort for sets of elements. In this report we extend 2LS with constructs... -
C-tableaux
The Nelson-Oppen combination method combines decision procedures for first-order theories satisfying certain conditions into a single decision procedure for the union... -
Strengthening the heart of an SMT-solver : Design and implementation of effic...
This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on... -
An Instantiation Scheme for Satisfiability Modulo Theories
International audience -
Coopération de procédures de décision : étude et implantation
Stage de DEA. || Le stage s'est fait en collaboration avec Silvio Ranise de l'équipe Cassis.. Rapport de stage. -
Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a New...
To appear in post-event proceedings. Colloque avec actes et comité de lecture. internationale.
