ahmed rezine

• Home
• Research
• Teaching
• Students

Associate professor ("docent") at Linköping University. I look for ways to extend automated verification techniques. Interests:

• model checking, abstract interpretation
• parameterized verification: concurrent, distributed systems
• shape analysis, heap manipulating programs
• concurrent data structures: fine grained, lock free
• cache coherence protocols, timing side-channel attacks

I lead the the CENIIT 12.04 research project about applying and extending automatic verification.

I co-investigate, with Prof.Sudipta Chattopadhyay, the Verification and Validation of Side-channel Freedom project project. The project members are grateful for the generous support of a highly competitive three-years grant from the Singapore Ministry of Education (MOE).

I am looking for clever and hard working students to carry out several exciting Master's and Bachelor theses. Contact me if interested or want to discuss a project.

News

• We are looking for two post-docs for the Verification and Validation of Side-channel Freedom project project. The selected candidates will work from the Singapore University of Technology and Design (SUTD).


• Our new work "On Reachability in Parameterized Phaser Programs", can be found here https://arxiv.org/pdf/1811.07142.pdf.


• Accepted conference paper. TRAU: SMT solver for string constraints, at the International Conference on Formal Methods in Computer-Aided Design, FMCAD 18.


• Accepted conference paper. Stability-aware integrated routing and scheduling for control applications in Ethernet networks, at Design, Automation and Test in Europe, DATE 2018.


• Accepted journal article. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures at the International Journal on Software Tools and Technology Transfer, volume 19, STTT 2017.


• Accepted conference paper. Safety Verification of Phaser Programs, at the International Conference on Formal Methods in Computer-Aided Design, FMCAD 17.


• Accepted conference paper. Quantifying the Information Leak in Cache Attacks via Symbolic Execution, at the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 17.


• Accepted conference paper. Flatten and Conquer (A Framework for Efficient Analysis of String Constraints), at the 38th annual ACM SIGPLAN conference on Programming Language Design and Implementation, PLDI 17.


• Accepted journal article. Counting dynamically synchronizing processes in International Journal on Software Tools for Technology Transfer, volume 18, STTT 16.