Using invariant functions and invariant relations to compute loop functions. - Lamia Labed Jilani; Olfa Mraihi; Asma Louhichi; Wided Ghardallou; Ali Mili 001 (ICSE (2), 2010)

Computing Preconditions and Postconditions of While Loops. - Olfa Mraihi; Wided Ghardallou; Asma Louhichi; Lamia Labed Jilani; Khaled Bsaïes; Ali Mili 001 (ICTAC, 2011)

Using invariant relations in the termination analysis of while loops. - Wided Ghardallou (ICSE, 2012)

A versatile concept for the analysis of loops. - Wided Ghardallou; Olfa Mraihi; Asma Louhichi; Lamia Labed Jilani; Khaled Bsaïes; Ali Mili 001 (J. Log. Algebraic Methods Program., 2012)

Invariant functions and invariant relations: An alternative to invariant assertions. - Lamia Labed Jilani; Olfa Mraihi; Asma Louhichi; Wided Ghardallou; Khaled Bsaïes; Ali Mili 001 (J. Symb. Comput., 2013)

Verifying while loops with invariant relations. - Asma Louhichi; Wided Ghardallou; Khaled Bsaïes; Lamia Labed Jilani; Olfa Mraihi; Ali Mili 001 (Int. J. Crit. Comput. Based Syst., 2014)

Relational Mathematics for Relative Correctness. - Jules Desharnais; Nafi Diallo; Wided Ghardallou; Marcelo F. Frias; Ali Jaoua; Ali Mili 001 (RAMiCS, 2015)

Correctness and Relative Correctness. - Nafi Diallo; Wided Ghardallou; Ali Mili 001 (ICSE (2), 2015)

Program Derivation by Correctness Enhacements. - Nafi Diallo; Wided Ghardallou; Jules Desharnais; Ali Mili 001 (Refine@FM, 2015)

Debugging without Testing. - Wided Ghardallou; Nafi Diallo; Ali Mili 001; Marcelo F. Frias (ICST, 2016)

Software Evolution by Correctness Enhancement. - Wided Ghardallou; Nafi Diallo; Ali Mili 001 (SEKE, 2016)

Relative Correctness: A Bridge Between Proving and Testing. - Wided Ghardallou; Ali Mili 001; Nafi Diallo (VECoS, 2016)

Program Repair by Stepwise Correctness Enhancement. - Nafi Diallo; Wided Ghardallou; Ali Mili 001 (PrePost@IFM, 2016)

What is a fault? and why does it matter? - Nafi Diallo; Wided Ghardallou; Jules Desharnais; Marcelo F. Frias; Ali Jaoua; Ali Mili 001 (Innov. Syst. Softw. Eng., 2017)

Projecting programs on specifications: Definition and implications. - Jules Desharnais; Nafi Diallo; Wided Ghardallou; Ali Mili 001 (Sci. Comput. Program., 2017)

Programming Without Refining. - Marwa Benabdelali; Lamia Labed Jilani; Wided Ghardallou; Ali Mili 001 (Refine@FM, 2018)

Convergence: Integrating termination and abort-freedom. - Nafi Diallo; Wided Ghardallou; Jules Desharnais; Ali Mili 001 (J. Log. Algebraic Methods Program., 2018)

Assume, Capture, Verify, Establish: Ingredients for Scalable Software Analysis. - Hessamaldin Mohammadi; Wided Ghardallou; Ali Mili 001 (QRS Companion, 2021)

Computing Program Functions. - Hessamaldin Mohammadi; Wided Ghardallou; Richard C. Linger; Ali Mili 001 (FormaliSE@ICSE, 2022)

Assume(), Capture(), Verify(), Establish(): A Vocabulary for Static Program Analysis. - Hessamaldin Mohammadi; Wided Ghardallou; Elijah Brick; Ali Mili 001 (QRS Companion, 2023)

Invariant Relations: A Bridge from Programs to Equations. - Wided Ghardallou; Hessamaldin Mohammadi; Elijah Brick; Ali Mili 001 (CoRR, 2023)

On the persistent rumors of the programmer's imminent demise. - Hessam Mohammadi; Wided Ghardallou; Elijah Brick; Ali Mili 001 (Softw. Syst. Model., 2023)

"Function Extraction: A New Paradigm for Producing Secure Code". - Richard C. Linger; Mark G. Pleszkoch; Jack McGaughey; John McHugh; Wided Ghardallou; Ali Mili 001 (NSPW, 2024)

Invariant relations for affine loops. - Wided Ghardallou; Hessamaldin Mohammadi; Richard C. Linger; Mark G. Pleszkoch; Ji Meng Loh; Ali Mili 001 (Acta Informatica, 2024)