Formal verification of a proof procedure for the description logic ALC. - Mohamed Chaabani; Mohamed Mezghiche; Martin Strecker (SCSS, 2012)

Logical Foundations for Reasoning about Transformations of Knowledge Bases. - Mohamed Chaabani; Rachid Echahed; Martin Strecker (ICTERI, 2013)

A Formalized Procedure for Database Horizontal Fragmentation in Isabelle/HOL Proof Assistant. - Cheikh Salmi; Mohamed Chaabani; Mohamed Mezghiche (MEDI, 2018)

Verified Path Indexing. - Mohamed Chaabani; Simon Robillard (CADE, 2025)