Tel: +46 (0)13 28 19 38
SE-581 83 LINKÖPING
Assistant professor ("universitetslektor") at
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
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.
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
Verification of Phaser Programs, at the International
Conference on Formal Methods in Computer-Aided Design, FMCAD
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
Constrained Monotonic Abstraction, at the 17th
International Conference on Verification, Model
Checking, and Abstract
and Counting Synchronizing Processes, at the 16th
International Conference on Verification, Model Checking, and
- Invited journal version (with proofs and details) of the
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
at the 26th International Conference on Computer Aided VerificationCAV 2014.
Counter-Abstraction: Refinable Subword Relations
for Parameterized Verification,
- ★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.