Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. - Amine Chaieb; Tobias Nipkow (LPAR, 2005)

Bytecode Analysis for Proof Carrying Code. - Martin Wildmoser; Amine Chaieb; Tobias Nipkow (Bytecode@ETAPS, 2005)

Verifying Mixed Real-Integer Quantifier Elimination. - Amine Chaieb (IJCAR, 2006)

Proof-Producing Program Analysis. - Amine Chaieb (ICTAC, 2006)

Context Aware Calculation and Deduction. - Amine Chaieb; Makarius Wenzel (Calculemus/MKM, 2007)

Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL. - Amine Chaieb (AISC/MKM/Calculemus, 2008)

Proof Synthesis and Reflection for Linear Arithmetic. - Amine Chaieb; Tobias Nipkow (J. Autom. Reason., 2008)

Automated methods for formal proofs in simple arithmetics and algebra (Automatische Methoden für formale Beweise in einfachen Arithmetiken und Algebren) - Amine Chaieb (2008)

Formal Power Series. - Amine Chaieb (J. Autom. Reason., 2011)