Forskningsinteresser

Forskningsområdene mine er formelle metoder, programvareverifisering, og didaktikk.

INF113 Innføring i operativsystem

INF100 Innføring i programmering

Vitenskapelig artikkel

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

Vitenskapelig Kapittel/Artikkel/Konferanseartikkel

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

Vitenskapelig foredrag

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

Se en full oversikt over publikasjoner i 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).