A. Armando, C. Castellini, E. Giunchiglia, and M. Maratea, A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints, Proc. SAT'04, 2004.
DOI : 10.1007/11527695_2

T. Ball, B. Cook, S. K. Lahiri, and L. Zhang, Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement, CAV, 2004.
DOI : 10.1007/978-3-540-27813-9_36

C. L. Barrett and S. Berezin, CVC Lite: A New Implementation of the Cooperating Validity Checker, Proc. CAV'04, 2004.
DOI : 10.1007/978-3-540-27813-9_49

M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. Van-rossum et al., An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic, Proc. TACAS'05, 2005.
DOI : 10.1007/978-3-540-31980-1_21

S. Cotton, E. Asarin, O. Maler, and P. Niebert, Some Progress in Satisfiability Checking for Difference Logic, Proc. FORMATS-FTRTFT 2004, 2004.
DOI : 10.1007/978-3-540-30206-3_19
URL : https://hal.archives-ouvertes.fr/hal-00157566

D. Deharbe and S. Ranise, Light-weight theorem proving for debugging and verifying units of code, First International Conference onSoftware Engineering and Formal Methods, 2003.Proceedings., 2003.
DOI : 10.1109/SEFM.2003.1236224

L. De-moura and H. Ruess, An Experimental Evaluation of Ground Decision Procedures, Proceedings of Computer-Aided Verification, p.4
DOI : 10.1007/978-3-540-27813-9_13

D. L. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, 2003.
DOI : 10.1145/1066100.1066102

J. Filliâtre, S. Owre, H. Rueß, and N. Shankar, ICS: Integrated Canonizer and Solver?, Proc. CAV'01, pp.246-249, 2001.
DOI : 10.1007/3-540-44585-4_22

H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, DPLL(T): Fast Decision Procedures, Proc. CAV'04, pp.175-188, 2004.
DOI : 10.1007/978-3-540-27813-9_14

C. Weidenbach and A. Nonnengart, Computing Small Clause Normal Forms, Hand. of Automated Reasoning, vol.1, 2001.