- E-mailcrystal.din@uib.no
- Visitor AddressThormøhlens gate 555006 BergenRoom406P1
- Postal AddressPostboks 78035020 Bergen
Research Interests
My research interests lie in the areas of formal methods, software verification, and didactics.
- (2024). Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages. ACM Transactions on Programming Languages and Systems. 1-58.
- (2023). Semantics-Based Version Control for Feature Model Evolution Plans. NIKT: Norsk IKT-konferanse for forskning og utdanning. 14 pages.
- (2023). Runtime Enforcement Using Knowledge Bases. Lecture Notes in Computer Science (LNCS). 220-240.
- (2023). Modular Soundness Checking of Feature Model Evolution Plans. Lecture Notes in Computer Science (LNCS). 417-437.
- (2022). Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins. Lecture Notes in Computer Science (LNCS). 188-204.
- (2022). I Can See Clearly Now: Clairvoyant Assertions for Deadlock Checking. Lecture Notes in Computer Science (LNCS). 1-18.
- (2020). Behavioral Contracts for Cooperative Scheduling. Lecture Notes in Computer Science (LNCS). 85-121.
- (2019). Translating active objects into colored Petri nets for communication analysis. Science of Computer Programming. 1-26.
- (2019). Geological Multi-scenario Reasoning. NIKT: Norsk IKT-konferanse for forskning og utdanning. 12 pages.
- (2019). Asynchronous Cooperative Contracts for Cooperative Scheduling. Lecture Notes in Computer Science (LNCS). 48-66.
- (2018). Program Verification for Exception Handling on Active Objects Using Futures. Lecture Notes in Computer Science (LNCS). 73-88.
- (2018). A modular reasoning system using uninterpreted predicates for code reuse. Journal of Logical and Algebraic Methods in Programming. 82-102.
- (2017). Translating Active Objects into Colored Petri Nets for Communication Analysis. Lecture Notes in Computer Science (LNCS). 84-99.
- (2017). Locally abstract, globally concrete semantics of concurrent programming languages. Lecture Notes in Computer Science (LNCS). 22-43.
- (2017). A Survey of Active Object Languages. ACM Computing Surveys. 39 pages.
- (2016). Session-based compositional analysis for actor-based languages using futures. Lecture Notes in Computer Science (LNCS). 296-312.
- (2015). History-Based Specification and Verification of Scalable Concurrent and Distributed Systems. Lecture Notes in Computer Science (LNCS). 217-233.
- (2015). Compositional reasoning about active objects with shared futures. Formal Aspects of Computing. 551-572.
- (2014). A sound and complete reasoning system for asynchronous communication with shared futures. Journal of Logic and Algebraic Programming. 360-383.
- (2012). Observable behavior of distributed systems: Component reasoning for concurrent objects. Journal of Logic and Algebraic Programming. 227-256.
- (2012). Compositional Reasoning about Shared Futures. Lecture Notes in Computer Science (LNCS). 94-108.
- (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.
- (2015). KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS.
- (2015). A Dynamic Logic with Traces and Coinduction.
- (2013). Comparison of Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. In proceedings of NWPT'13.
- (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects.
- (2021). Three-Way Semantic Merge for Feature Model Evolution Plans.
- (2021). Modular Soundness Checking of Feature Model Evolution Plans.
- (2022). Subsurface Evaluation Through Multi-scenario Reasoning. 31 pages.
- (2020). Consistency-Preserving Evolution Planning on Feature Models. 12 pages.
- (2014). Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. 8 pages.
- (2013). A comparison of runtime assertion checking and theorem proving forconcurrent and distributed systems. 3 pages.
- (2012). Soundness of a Reasoning System for Asynchronous Communication with Futures. 3 pages.
- (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects. 2 pages.
- (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects. 2 pages.
More information in national current research information system (CRIStin)
Guest Editor
I am the guest editor of special issue on the Nordic Workshop on Programming Theory (NWPT 2022).
Local Organizer
Program Chair
I am the chair of NIK 2023, which is the Norwegian Informatics Conference under NIKT.
I am the PhD Symposium Chair for iFM 2023.
Program Committee
I was the part of the Program Committee for
- 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
I was also a member of the ECOOP 2021 Artifact Evaluation Committee.
I am a reviewer of the journal 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).