crystald

Hjemmeside
Faglige interesser
Jeg er interessert i formelle metoder, analyse og verifisering av programvaresystemer. Jeg utviklet et "compositional reasoning system" for paralelle og distribuerte systemer. For tiden er jeg involvert i Geological Assistant-prosjektet ved SIRIUS forskningssenter.
Undervisning
INF4140 - Models of Concurrency
INF9140 - Symbolic CTL Model Checking
INF2220 - Algorithms and Data Structures
Bachelorkurs - Introduction to Programming
Doktorgradsprøveforelesning - Formal Verification of Real-Time Systems
Bakgrunn
Forsker ved SIRIUS Research Center, May 2019 - nå,
University of Oslo, Norway
Postdoc i Computer Science, March 2016 - March 2019,
University of Oslo, Norway
Postdoc i Computer Science, April 2014 - Feb 2016,
TU Darmstadt, Germany
Project assistant, Jul 2009 - Dec 2009, SEFM forskergruppe,
Chalmers Tekniska Högskola, Sverige
M.Sc. i Software Engineering, Sep 2007 - Jun 2009,
Chalmers Tekniska Högskola, Sverige
B.Sc. i Computer Science, Sep 2005 - Jun 2008,
National Chiao Tung University, Taiwan
Publikasjoner
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. The Joural 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)
- Hoff, Adrian; Nieke, Michael; Seidl, Christoph; Sæther, Eirik Halvard; Motzfeldt, Ida Sandberg; Din, Crystal Chang; Yu, Ingrid Chieh & Schaefer, Ina (2020). Consistency-Preserving Evolution Planning on Feature Models, In Roberto Erick Lopez-Herrejon (ed.), SPLC'20: 24th ACM International Systems and Software Product Line Conference, Montreal, Quebec, Canada, October 19-23, 2020, Volume A. Association for Computing Machinery (ACM). ISBN 978-1-4503-7569-6. research article. s 8:1 - 8:12 Fulltekst i vitenarkiv.
- Kamburjan, Eduard; Din, Crystal Chang; Hähnle, Reiner & Johnsen, Einar Broch (2020). Behavioral Contracts for Cooperative Scheduling. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 12345, s 85- 121 . doi: 10.1007/978-3-030-64354-6_4
- Din, Crystal Chang; Karlsen, Leif Harald; Pene, Irina; Stahl, Oliver; Yu, Ingrid Chieh & Østerlie, Thomas (2019). Geological Multi-scenario Reasoning. NIKT: Norsk IKT-konferanse for forskning og utdanning. ISSN 1892-0713. Fulltekst i vitenarkiv.
- Gkolfi, Anastasia; Din, Crystal Chang; Johnsen, Einar Broch; Kristensen, Lars Michael; Steffen, Martin & Yu, Ingrid Chieh (2019). Translating active objects into colored Petri nets for communication analysis. Science of Computer Programming. ISSN 0167-6423. 181, s 1- 26 . doi: 10.1016/j.scico.2019.04.002
- Kamburjan, Eduard; Din, Crystal Chang; Hahnle, Reiner & Johnsen, Einar Broch (2019). Asynchronous Cooperative Contracts for Cooperative Scheduling. Lecture Notes in Computer Science (LNCS). 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 (LNCS). ISSN 0302-9743. 10886, s 73- 88 . doi: 10.1007/978-3-319-92970-5_5 Fulltekst i vitenarkiv.
- 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 Fulltekst i vitenarkiv.
- Din, Crystal Chang; Hahnle, Reiner; Johnsen, Einar Broch; Pun, Ka I & Tapia Tarifa, Silvia Lizeth (2017). Locally abstract, globally concrete semantics of concurrent programming languages. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 10501 LNAI, s 22- 43 . doi: 10.1007/978-3-319-66902-1_2
- 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 (LNCS). 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 (LNCS). ISSN 0302-9743. 10009 LNCS, s 296- 312 . doi: 10.1007/978-3-319-47846-3_19
- Din, Crystal Chang & Owe, Olaf (2015). Compositional reasoning about active objects with shared futures. Formal Aspects of Computing. ISSN 0934-5043. 27(3), s 551- 572 . doi: 10.1007/s00165-014-0322-y
- Din, Crystal Chang; Tapia Tarifa, Silvia Lizeth; Hähnle, Reiner & Johnsen, Einar Broch (2015). History-Based Specification and Verification of Scalable Concurrent and Distributed Systems. Lecture Notes in Computer Science (LNCS). ISSN 0302-9743. 9407, s 217- 233 . doi: 10.1007/978-3-319-25423-4_14
- 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 (LNCS). 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; Dovland, Johan; Johnsen, Einar Broch & Owe, Olaf (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. Extended abstract. s 26 - 27
- 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
- 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.
- Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch & Owe, Olaf (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects.