Education

Ph.D. in Computer Science 2012-2016

CEA-List & CNAM-Cédric France


Master Degree in Information Sciences and Systems 2010-2011

Aix-Marseille University France


Engineer Degree in Computer Networking and Telecommunications 2005-2011

National Institute of Applied Sciences and Technology Tunisia


Experiences

IRT-SystemX Palaiseau

R&D Engineer Sept 17 - Now

Formal modelling and verification of the security policies of a real-time operating system

Keywords: Formal specification of memory model, spatial and temporal properties, theorem proving, proofs, model checking

CNAM Paris

Teaching assistant 2015-2016

  • - Concurrent applications: design and tools

CEA-List, L3S Lab Palaiseau

PhD candidate 2012-2016

The thesis proposes a formal approach to specify and verify critical systems, in particular software systems implemented with C. Such systems are hard to verify due to the concurrency and the low level aspects of C. We address these issues by modeling the semantics of C and using refinement and abstraction techniques in order to tackle the complexity of the verification process.

Advisors: Matthieu Lemerre, Belgacen Ben Hedia, Serge Haddad, Kamel Barkaoui

Polytech' Paris Sud Orsay

Teaching assistant 2012-2015

  • - Computer Networks (M1Miage / L3-Info / ET3-Info)

  • - Operating Systems (L3-Info)

Information Sciences and Systems Lab Marseille

Research Intern Jan - June 11

Integration of a multicriteria decision system for controlling individuals flow in restricted area

Information Sciences and Systems Lab Marseille

Research Intern Sept - Dec 10

Contribution to the development of holonic control of people flow

Netsystem Tunis

Engineering Intern Jun - Jul 09

Development of an electronic document management system with SharePoint

INBMI Tunis

Intern Jul - Aug 07

Network Administration and Router Configuration

My thesis

Description

The thesis proposes a formal approach to specify and verify critical systems, in particular software systems implemented with C. Such systems are hard to verify due to the concurrency and the low level aspects of C. We address these issues by modeling the semantics of C and using refinement and abstraction techniques in order to tackle the complexity of the verification process.

Publications

Verifying and Constructing Abstract TLA Specifications: Application to the Verification of C programs

A. Methni, M. Lemerre, B. Ben Hedia, S. Haddad and K. Barkaoui.

In the Tenth International Conference on Software Engineering Advances, Barcelone, Spain, November 2015.

State Space Reduction Strategies for Model Checking Concurrent C Programs

A. Methni, M. Lemerre, B. Ben Hedia, S. Haddad and K. Barkaoui.

In Formal Techniques for Safety-Critical Systems, Communications in Computer and Information Science 476, pages 206-222. Springer, 2015.

Specifying and Verifying Concurrent C Programs with TLA+

A. Methni, M. Lemerre, B. Ben Hedia, S. Haddad and K. Barkaoui.

In FTSCS, the 3rd International Workshop on Formal Techniques for Safety-Critical Systems, Luxembourg, 2014.

An Approach for Verifying Concurrent C Programs

A. Methni, M. Lemerre, B. Ben Hedia, S. Haddad and K. Barkaoui.

In JRWRTC'14, the 8th Junior Researcher Workshop on Real-Time Computing, Versailles, France, 2014.

Traduction automatique du code C vers TLA+.

A. Methni, M. Lemerre, B. Ben Hedia, S. Haddad and K. Barkaoui.

In ETR’13, Ecole Temps Réel, Toulouse, 2013.

Contrôle intelligent et isoarchique de flux de personnes basé sur la biométrie et l’infotronique

T. Louati, A. Methni, F. Ounnar, P. Pujo, C. Pistoresi.

In CIGI’11, 9e Congrès International de Génie Industriel, Québec, Canada, 2011.

Software

C2TLA+

Is a Frama-C plug-in. It translates a given (subset of) C code into TLA+ (Temporal Logic of Actions) specification, on which back-end verification techniques can be applied to check a set of properties.

Other contributions

Talks

Méthode de conception de logiciel système critique couplée à une démarche de vérification formelle

ACTRISS (ACtion Temps Réel : Infrastructures et Services Systèmes) March, 2015 MeFoSyLoMa (Méthodes formelles pour les systèmes logiciels et matériels) May, 2016

Specifying and Verifying Concurrent C Programs with TLA+

GT-Verif (French national working group) June, 2014

C2TLA+ – A translator from C to TLA+

TLA+ Community Event June, 2014

Commitees

Member of the program committee (student session) of Ecole Temps Réel (ETR’15), Rennes 2015

Member of the local organization committee of the 22nd International Conference on Real-Time Networks and Systems, Versailles 2014 .

Miscellaneous

Languages

Arabic (Native), French (Fluent), English (Professional ).

Memberships

  • - Computer Security Club (Securinets) 2007-2011 Tunis
             Vice president 2008-2010

Sport

Diving

Get In Touch.

If you want to discuss about my work please contact me on my mail methni.amira[at]gmail.com