ahmed rezine
firstname.lastname@liu.se
Tel: +46 (0)13 28 19 38
Linköping University
SE-581 83 LINKÖPING
Assistant professor ("universitetslektor") 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, 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. Contact me if interested or want to discuss a project.
News
-
Accepted Quantifying
the Information Leak in Cache Attacks via Symbolic
Execution, at the 15th ACM-IEEE International Conference
on Formal Methods and Models for System Designn, MEMCODE 17
-
Accepted Safety
Verification of Phaser Programs, at the International
Conference on Formal Methods in Computer-Aided Design, FMCAD
17
-
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.