ahmed.rezine[email]liu.se (gpg) Tel: +46 (0)13 28 19 38 Fax: +46 (0)13 14 94 03 Linköping University SE-581 83 LINKÖPING
Forskarassistent (Assistant Professor) at ESLAB/ Department of Computer and Information Science in Linköping. I look in my research for ways to extend automated verification techniques in general, and Model Checking in particular, to systems with unbounded state spaces. Examples include verification of parameterized concurrent and distributed systems and heap manipulating programs.
In my Parisian post-doc (LIAFA) I worked on the verification of sequential programs with dynamic heaps. This was followed by my Uppsala post-doc (UPMARC-initiative) where I worked on the applications of verification to multicore systems. I obtained my thesis, about the verification of parameterized systems, under the supervision of Prof.Parosh Abdulla from Uppsala University. I obtained my Engineering degree from Tunisia's Polytechnic School.
Leader of the CENIIT 12.04 research project.
News
- An Integrated Specification and Verification Technique for Highly Concurrent Data Structures to appear at TACAS 2013.
- Memorax: Fence Inference under the TSO Memory Model to appear at TACAS 2013.
- Verifying Safety and Liveness for the FlexTM Hybrid Transactional Memory to appear at DATE 2013.
- Automatic Test Program Generation for Out-of-Order Superscalar Processors at ATS 2012.
- Automatic Fence Insertion in Integer Programs via Predicate Abstraction at SAS 2012.
- Ordered Counter Abstraction, a new family of infinite abstractions for parameterized verification.
- Several Masters and Bachelor thesis projects are available here. Do not hesitate to contact me ! if you want to discuss these or other projects.
- Counter-Example Guided Fence Insertion under TSO at TACAS 2012.
- Consider participating to the Infinity 2012 workshop collocated with Formal Methods 2012 in ... CNAM-Paris!
| Publications | Teaching | Students | Tools |
Publications
Journals
- A lightweight regular model checking approach for parameterized systems in STTT 2012.
- Automatic verification of directory-based consistency protocols with graph constraints in IJFCS 2011.
- Approximated parameterized verification of infinite-state processes with global conditions in FMSD 2009.
- Monotonic abstraction: on efficient verification of parameterized systems in IJFCS 2009
- Tree regular model checking: A simulation-based approach in JLAP 2006.
Conferences
- Automatic Fence Insertion in Integer Programs via Predicate Abstraction at SAS 2012.
- Automatic Test Program Generation for Out-of-Order Superscalar Processors at ATS 2012.
- Counter-Example Guided Fence Insertion under TSO at TACAS 2012.
- Invariant synthesis for programs manipulating lists with unbounded data at CAV 2010.
- Constrained monotonic abstraction: a cegar for parameterized verification at CONCUR 2010.
- Automatic verification of directory-based consistency protocols at RP 2009.
- Approximated context-sensitive analysis for parameterized verification at FORTE 2009.
- Monotonic abstraction in action at ICTAC 2008.
- Monotonic abstraction for programs with dynamic memory heaps at CAV 2008.
- Parameterized tree systems at FORTE 2008.
- Handling parameterized systems with non-atomic global conditions at VMCAI 2008.
- Parameterized verification of infinite-state processes with global conditions at CAV 2007.
- Regular model checking without transducers (on efficient verification of parameterized systems) at TACAS 2007
- Proving liveness by backwards reachability at CONCUR 2006.
- Simulation-based iteration of tree transducers at TACAS 2005.
Technical reports
- Ordered Counter Abstraction.
- Software Model Checking for GPGPU Programs, Towards a Verification Tool.
Teaching
- I supervise and teach the Objektorienterad programmering course for HT'2012.
Previous Teachings
- Programming Theory (B3,Masters)
- Distributed Systems (Masters)
- Design patterns
- Computer Architecture (B1,B2)
Masters Projects
Several Masters and Bachelor thesis projects are available here. Do not hesitate to contact me ! if you want to discuss these or other projects.Current Students
- Rizwan Abbasi
Previous Students
- Ala Omer Ahmed
- Majid Khorsandi Aghai
- Mehmet Ali Arslan
Tools
I am developing a new prototype PCW to experiment with an original adaptation of counter abstraction for the verification of parameterized systems.
I develop UNDIP for the verification of safety properties for Unbounded Distributed Parametreized systems. UNDIP is a generalization of PFS which verifies the same type of properties for Parameterized Finite state Systems.