Tel: +46 (0)13 28 19 38
SE-581 83 LINKÖPING
Associate professor ("universitetslektor") at
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
I am looking for clever and hard working
students to carry out several exciting Master's
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.