ahmed rezine

• Home
• Research
• Teaching
• Students
• Tools

Associate professor ("universitetslektor") at Linköping University. I look for ways to extend automated verification techniques to computer systems with state spaces of arbitrary sizes:

• model checking, abstract interpretation
• parameterized verification: concurrent, distributed systems
• shape analysis, heap manipulating programs
• highly concurrent data structures: fine grained, lock free
• cache coherence protocols, weak memory models

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

I am looking for clever and hard working students to carry out several exciting Master's and Bachelor thesis projects.

News

• Accepted 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 Lazy Constrained Monotonic Abstraction, at the 17th International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI 2016.
• Accepted Abstracting and Counting Synchronizing Processes, at the 16th International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI 2015.
• Invited journal version (with proofs and details) of the paper An Integrated Specification and Verification Technique for Highly Concurrent Data Structures.STTT'16.
• Invited journal version (with all proofs and detailed descriptions of the examples) of the paper Ordered Counter-Abstraction: Refinable Subword Relations for Parameterized Verification. STTT'16.
• Accepted String Constraints for Verification, at the 26th International Conference on Computer Aided VerificationCAV 2014.
• Ordered Counter-Abstraction: Refinable Subword Relations for Parameterized Verification, LATA 2014.
• ★Best paper award★, An Integrated Specification and Verification Technique for Highly Concurrent Data Structures, 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, DATE 2013.