Name : Crystal Chang Din
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