ahmed rezine
firstname.lastname@liu.se Tel: +46 (0)13 28 19 38 Linköping University SE-581 83 LINKÖPINGAssociate 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
- concurrent and heap manipulating data structures: fine grained, lock free
- cache coherence protocols and memory consistency
- timing side-channel attacks
News
- Accepted conference paper. On reachability in parameterized phaser programs at Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2019.
- Accepted journal article. Quantifying the Information Leakage in Cache Attacks via Symbolic Execution at ACM Transactions on Embedded Computing Systems (TECS) 2019.
- Accepted journal article. Software-based Self-Testing using Bounded Model Checking for Out-of-Order Superscalar Processors at IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2019.
- I co-investigate, with Prof.Sudipta Chattopadhyay, the Verification and Validation of Side-channel Freedom project. The project members are grateful for the generous support of a highly competitive three-years grant from the Singapore Ministry of Education (MOE).
- 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.