Position : Postdoctoral Fellow

Research group : Precise modeling and analysis (PMA)

Institution : Institutt for informatikk

Adress: Institutt for informatikk

Universitetet i Oslo

Postboks 1080 Blindern

N-0316 Oslo Norway

Room : 8168 Ole-Johan Dahls hus

Office number : +47 22 84 08 52

E-mail : crystald(at)ifi.uio.no

DBLP : Publications

Teaching assistant : INF4140 - Models of Concurrency (Autumn 2010)

Teaching assistant : INF4140 - Models of Concurrency (Autumn 2011)

Lecturer : INF4140 - Models of Concurrency (Autumn 2012)

Research report 401: Observable Behavior of Distributed Systems

Research report 415: An Approach to Compositional Reasoning about Concurrent Objects and Futures

Research report 435: A Comparison of Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems

Research report 437: Compositional and Sound Reasoning about Active Objects with Shared Futures

Presentation (NWPT'10) : Observable Behavior of Distributed Systems : Component Reasoning for Concurrent Objects

Presentation (COST Action) : Compositional Reasoning about Concurrent Objects and Futures

Presentation (SEFM'12) : Compositional Reasoning about Concurrent Objects and Futures

Presentation (NWPT'12) : A Sound Reasoning System for Asynchronous Communication with Shared Futures

Presentation (NWPT'13) : A Comparison of Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems

Presentation (MODELSWARD'14) : Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems

Presentation (INF9140 Model Checking) : Symbolic CTL Model Checking

NWPT10 : Observable Behavior of Distributed Systems : Component Reasoning for Concurrent Objects

NWPT12 : Soundness of a Reasoning System for Asynchronous Communication with Futures

NWPT13 : A Comparison of Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems

JLAP paper : Observable Behavior of Distributed Systems: Component Reasoning for Concurrent Objects

JLAMP paper : A Sound and Complete Reasoning System for Asynchronous Communication with Shared Futures

SEFM paper (2014) : Compositional Reasoning about Shared Futures

MODELSWARD paper (2014) : Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems

FAC paper (2015): Compositional reasoning about active objects with shared futures

TABLEAUX paper (2015) : A Dynamic Logic with Traces and Coinduction

SEFM paper (2015) : History-Based Specification and Verification of Scalable Concurrent and Distributed Systems

Master Thesis (2009) : Testing Erlang-OTP with QuickCheck

KeY-ABS (A theorem prover for concurrent and distributed ABS programs) :

Tool : KeY-ABS Tool Download

Paper : KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS

Tutorial : KeY-ABS Tutorial

Example : Banking Account Example (Implementation and Specification)

Screencast : The Screencast for the Banking Account Example

Last modified: Tue Nov 16 11:15:19 CET 2010