Research Interests

My research interests lie in the areas of formal methods, software verification, and didactics.

INF113 Introduction to Operating Systems

INF100 Introduction to Programming

Academic article

• Din, Crystal Chang; Hähnle, Reiner; Henrio, Ludovic et al. (2024). Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages. (external link)
• Motzfeldt, Ida Sandberg; Yu, Ingrid Chieh; Din, Crystal Chang et al. (2023). Modular Soundness Checking of Feature Model Evolution Plans. (external link)
• Kamburjan, Eduard; Din, Crystal Chang (2023). Runtime Enforcement Using Knowledge Bases. (external link)
• Sæther, Eirik Halvard; Yu, Ingrid Chieh; Din, Crystal Chang (2023). Semantics-Based Version Control for Feature Model Evolution Plans. (external link)
• Abusdal, Ole Jørgen; Din, Crystal Chang; Pun, Violet Ka I et al. (2022). I Can See Clearly Now: Clairvoyant Assertions for Deadlock Checking. (external link)
• Kamburjan, Eduard; Din, Crystal Chang; Schlatte, Rudolf et al. (2022). Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins. (external link)
• Kamburjan, Eduard; Din, Crystal Chang; Hähnle, Reiner et al. (2020). Behavioral Contracts for Cooperative Scheduling. (external link)
• Gkolfi, Anastasia; Din, Crystal Chang; Johnsen, Einar Broch et al. (2019). Translating active objects into colored Petri nets for communication analysis. (external link)
• Din, Crystal Chang; Karlsen, Leif Harald; Pene, Irina et al. (2019). Geological Multi-scenario Reasoning. (external link)
• Kamburjan, Eduard; Din, Crystal Chang; Hahnle, Reiner et al. (2019). Asynchronous Cooperative Contracts for Cooperative Scheduling. (external link)
• Din, Crystal Chang; Johnsen, Einar Broch; Owe, Olaf et al. (2018). A modular reasoning system using uninterpreted predicates for code reuse. (external link)
• Chang Din, Crystal; Schlatte, Rudolf; Chen, Tzu-Chun (2018). Program Verification for Exception Handling on Active Objects Using Futures. (external link)
• de Boer, Frank; Serbanescu, Vlad; Hähnle, Reiner et al. (2017). A Survey of Active Object Languages. (external link)
• Gkolfi, Anastasia; Din, Crystal Chang; Johnsen, Einar Broch et al. (2017). Translating Active Objects into Colored Petri Nets for Communication Analysis. (external link)
• Din, Crystal Chang; Hahnle, Reiner; Johnsen, Einar Broch et al. (2017). Locally abstract, globally concrete semantics of concurrent programming languages. (external link)
• Kamburjan, Eduard; Din, Crystal Chang; Chen, Tzu-Chun (2016). Session-based compositional analysis for actor-based languages using futures. (external link)
• Din, Crystal Chang; Owe, Olaf (2015). Compositional reasoning about active objects with shared futures. (external link)
• Din, Crystal Chang; Tapia Tarifa, Silvia Lizeth; Hähnle, Reiner et al. (2015). History-Based Specification and Verification of Scalable Concurrent and Distributed Systems. (external link)
• Din, Crystal Chang; Owe, Olaf (2014). A sound and complete reasoning system for asynchronous communication with shared futures. (external link)
• Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch et al. (2012). Observable behavior of distributed systems: Component reasoning for concurrent objects. (external link)
• Din, Crystal Chang; Dovland, Johan; Owe, Olaf (2012). Compositional Reasoning about Shared Futures. (external link)
• Din, Crystal Chang; Bubel, Richard; Hähnle, Reiner (2010). Verification of Variable Software: an Experience Report. (external link)

Academic chapter/article/Conference paper

• Yu, Ingrid Chieh; Pene, Irina; Din, Crystal Chang et al. (2022). Subsurface Evaluation Through Multi-scenario Reasoning. (external link)
• Hoff, Adrian; Nieke, Michael; Seidl, Christoph et al. (2020). Consistency-Preserving Evolution Planning on Feature Models. (external link)
• Din, Crystal Chang; Owe, Olaf; Bubel, Richard (2014). Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. (external link)
• Din, Crystal Chang; Bubel, Richard; Owe, Olaf (2013). A comparison of runtime assertion checking and theorem proving forconcurrent and distributed systems. (external link)
• Din, Crystal Chang; Owe, Olaf (2012). Soundness of a Reasoning System for Asynchronous Communication with Futures. (external link)
• Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch et al. (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects. (external link)
• Din, Crystal Chang; Dovland, Johan; Owe, Olaf et al. (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects. (external link)

Academic lecture

• Din, Crystal Chang; Bubel, Richard; Hähnle, Reiner (2015). KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS. (external link)
• Bubel, Richard; Din, Crystal Chang; Hähnle, Reiner et al. (2015). A Dynamic Logic with Traces and Coinduction. (external link)
• 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. (external link)
• Din, Crystal Chang; Dovland, Johan; Johnsen, Einar Broch et al. (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects. (external link)

See a complete overview of publications in Cristin.

Gjesteredaktør

Jeg er gjesteredaktør for Nordic Workshop on Programming Theory (NWPT 2022) special issue.

Lokalt arrangør

• KeY Symposium 2023
• NWPT 2022

Programleder

Jeg er leder av NIK 2023, som er Norsk Informatikkkonferanse under NIKT.

Jeg er PhD Symposium Chair til iFM 2023.

Programkomiteen

Jeg var en del av programkomiteen til 

• Software Verification and Testing Track (SVT) of the 38th Annual ACM Symposium on Applied Computing (SAC 2024)
• Software Verification and Testing Track (SVT) of the 38th Annual ACM Symposium on Applied Computing (SAC 2023)
• NWPT 2023
• NWPT 2022
• ICT Research School Annual Meeting 2022
• TheWebConf 2022
• UDIT 2021

Jeg var også medlem av ECOOP 2021 Artifact Evaluation Committee.

Jeg er en anmelder til journalen Formal Aspects of Computing.

In software engineering, demand of customers for configuration options that address various different business concerns creates the need to manage variability by developing not just a single software system but, in fact, an entire family of software systems with similar functionality. Software Product Line (SPL) engineering is a software engineering method to efficiently develop a family of software systems by capitalizing on their similarities while explicitly handling their differences. Due to the size and complexity of these systems, SPLs constitute a major investment with long-term strategic value. Over time, SPLs have to be adapted as part of software evolution to address new requirements, which is particularly complicated as an entire software family has to be adapted. 

While existing approaches (https://dl.acm.org/doi/10.1145/3382025.3414964) can identify the evolution paradoxes in an evolution plan of SPLs and can analyse whether an evolution plan will satisfy the given requirements, there is still lacking support for explaining why the business requirements cannot be satisfied (Thesis A). Furthermore, instead of rigorously prohibiting problematic changes, we may devise a flexible method that determines appropriate additional changes to perform to still reach the intended evolution goal when possible (Thesis B). An SPL can be defined in terms of multiple configurable features structured within a feature model, which also specifies feature dependencies. We would like to extend the current work so that feature dependencies are also taken into account in the reachability analysis of software evolution planning (Thesis C).