Crystal Chang Din

Image of Crystal Chang Din
Norwegian version of this page
Phone +47-22845516
Room 8270
Username
Visiting address Gaustadalleen 23 B None 0373 OSLO
Postal address Postboks 1080 Blindern 0316 OSLO

Homepage

http://folk.uio.no/crystald/

Academic Interests

I am interested in formal methods, program analysis and verification of software systems. I developed a compositional reasoning system for concurrent and distributed systems. Currently, I am involved in the Geological Assistant project at the SIRIUS Research Centre. The project’s goal is to develop a tool-supported method for exploration geologists to better assess and evaluate exploration prospects by applying established techniques from knowledge representation and formal methods from software verification. The project includes researchers from the University of Oslo and NTNU with expertise ranging from implementation and use of digital technologies, knowledge representation, formal methods, and naturally, geology.

Teaching

INF4140 - Models of Concurrency

INF9140 - Symbolic CTL Model Checking

INF2220 - Algorithms and Data Structures 

Bachelor course - Introduction to Programming 

PhD defense trial lecture - Formal Verification of Real-Time Systems

Higher education and employment history

Researcher at the SIRIUS Research Centre, May 2019 - present,

University of Oslo, Norway

Postdoc in Computer Science, March 2016 - March 2019,

University of Oslo, Norway

Postdoc in Computer Science, April 2014 - Feb 2016, 

TU Darmstadt, Germany

Ph.D. in Computer Science, Feb 2010 - April 2014,

PMA research group,

University of Oslo, Norway

Project assistant, Jul 2009 - Dec 2009, SEFM research group,

Chalmers University of Technology, Sweden

M.Sc. in Software Engineering, Sep 2007 - Jun 2009,

Chalmers University of Technology, Sweden

B.Sc. in Computer Science, Sep 2005 - Jun 2008,

National Chiao Tung University, Taiwan

 

Tags: formal methods, verification, concurrency, Object-orientation

Publications

Din, Crystal Chang; Owe, Olaf & Bubel, Richard (2014). Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. MODELSWARD 2014, SCITEPRESS.

Din, Crystal Chang; Dovland, Johan & Owe, Olaf (2012). Compositional Reasoning about Shared Futures. SEFM 2012, LNCS 7504, pp. 94–108, 2012 [http://link.springer.com/chapter/10.1007/978-3-642-33826-7_7]

Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch & Owe, Olaf (2012). An Approach to Compositional Reasoning about Concurrent Objects and Futures
. Research report 415. Department of Informatics, University of Oslo, Norway. Feb 2012. [Report]

Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch & Owe, Olaf (2012). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects. Journal of Logic and Algebraic Programming. @ Elsevier 2012. [Link]

Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch & Owe, Olaf (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects. Research report 401. Department of Informatics, University of Oslo, Norway. Nov 2010. [Report]

Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch & Owe, Olaf (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects, In Marina, Walden & Luigia, Petre (ed.),  Proceedings of the 22nd Nordic Workshop on Programming Theory, NWPT'10.  TUCS.  ISBN 978-952-12-2478-2.  Extended abstract.  s 26 - 27

Bubel, Richard; Din, Crystal Chang & Hähnle, Reiner (2010). Verification of Variable Software: an Experience Report
Pre-proceedings. International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Paris, France, FoVeOOS 2010 (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.167.1149)

 

  • Kamburjan, Eduard; Din, Crystal Chang; Hahnle, Reiner & Johnsen, Einar Broch (2019). Asynchronous Cooperative Contracts for Cooperative Scheduling. Lecture Notes in Computer Science.  ISSN 0302-9743.  11724 LNCS, s 48- 66 . doi: 10.1007/978-3-030-30446-1_3
  • Chang Din, Crystal; Schlatte, Rudolf & Chen, Tzu-Chun (2018). Program Verification for Exception Handling on Active Objects Using Futures. Lecture Notes in Computer Science.  ISSN 0302-9743.  10886, s 73- 88 . doi: 10.1007/978-3-319-92970-5_5
  • Din, Crystal Chang; Johnsen, Einar Broch; Owe, Olaf & Yu, Ingrid Chieh (2018). A modular reasoning system using uninterpreted predicates for code reuse. Journal of Logical and Algebraic Methods in Programming.  ISSN 2352-2208.  95, s 82- 102 . doi: 10.1016/j.jlamp.2017.11.004
  • de Boer, Frank; Serbanescu, Vlad; Hähnle, Reiner; Henrio, Ludovic; Rochas, Justine; Din, Crystal Chang; Johnsen, Einar Broch; Sirjani, Marjan; Khamespanah, Ehsan; Fernandez-Reyes, Kiko & Yang, Albert Mingkun (2017). A Survey of Active Object Languages. ACM Computing Surveys.  ISSN 0360-0300.  50(5) . doi: 10.1145/3122848
  • Gkolfi, Anastasia; Din, Crystal Chang; Johnsen, Einar Broch; Steffen, Martin & Yu, Ingrid Chieh (2017). Translating Active Objects into Colored Petri Nets for Communication Analysis. Lecture Notes in Computer Science.  ISSN 0302-9743.  (10522), s 84- 99 . doi: 10.1007/978-3-319-68972-2_6
  • Kamburjan, Eduard; Din, Crystal Chang & Chen, Tzu-Chun (2016). Session-based compositional analysis for actor-based languages using futures. Lecture Notes in Computer Science.  ISSN 0302-9743.  10009 LNCS, s 296- 312 . doi: 10.1007/978-3-319-47846-3_19
  • Din, Crystal Chang & Owe, Olaf (2014). A sound and complete reasoning system for asynchronous communication with shared futures. Journal of Logic and Algebraic Programming.  ISSN 1567-8326.  83(5-6), s 360- 383 . doi: 10.1016/j.jlamp.2014.03.003
  • Din, Crystal Chang; Owe, Olaf & Bubel, Richard (2014). Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems, In Joaquim Filipe & R. Neves (ed.),  Proc. International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2014.  SciTePress.  ISBN 978-989-8565-42-6.  Chapter.  s 480 - 487
  • Din, Crystal Chang; Bubel, Richard & Owe, Olaf (2013). A comparison of runtime assertion checking and theorem proving forconcurrent and distributed systems, In Tarmo Uustalu & Jüri Vain (ed.),  25th Nordic Workshop on Programming TheoryNWPT 2013, Tallinn, Estonia, 20–22 November 2013Abstracts.  Institute of Cybernetics at Tallinn University of Technology.  ISBN 978-9949-430-70-3.  abstract.  s 25 - 27
  • Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch & Owe, Olaf (2012). Observable behavior of distributed systems: Component reasoning for concurrent objects. Journal of Logic and Algebraic Programming.  ISSN 1567-8326.  81(3), s 227- 256 . doi: 10.1016/j.jlap.2012.01.003
  • Din, Crystal Chang; Dovland, Johan & Owe, Olaf (2012). Compositional Reasoning about Shared Futures. Lecture Notes in Computer Science.  ISSN 0302-9743.  7504, s 94- 108 . doi: 10.1007/978-3-642-33826-7_7
  • Din, Crystal Chang & Owe, Olaf (2012). Soundness of a Reasoning System for Asynchronous Communication with Futures, In Uwe Egbert Wolter & Yngve Lamo (ed.),  24th Nordic Workshop on Programming Theory.  Universitetet i Bergen.  kapitt.
  • Din, Crystal Chang; Bubel, Richard & Hähnle, Reiner (2010). Verification of Variable Software: an Experience Report. Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France.  ISSN 2190-4782.
  • Din, Crystal Chang; Dovland, Johan; Owe, Olaf & Johnsen, Einar Broch (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects, In Marina Walden & Luigia Petre (ed.),  Proceedings of the 22nd Nordic Workshop on Programming Theory, NWPT'10.  TUCS.  ISBN 978-952-12-2478-2.  kapitt.  s 26 - 27

View all works in Cristin

  • Bubel, Richard; Din, Crystal Chang; Hähnle, Reiner & Nakata, Keiko (2015). A Dynamic Logic with Traces and Coinduction.
  • Din, Crystal Chang; Bubel, Richard & Hähnle, Reiner (2015). KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS.
  • Din, Crystal Chang; Bubel, Richard & Owe, Olaf (2013). Comparison of Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. In proceedings of NWPT'13.

View all works in Cristin

Published Nov. 4, 2010 1:50 PM - Last modified Oct. 2, 2019 8:22 PM