Hjem
Crystal Chang Dins bilde

Crystal Chang Din

Førsteamanuensis
  • E-postcrystal.din@uib.no
  • Besøksadresse
    Thormøhlens gate 55
    5006 Bergen
    Rom 
    406P1
  • Postadresse
    Postboks 7803
    5020 Bergen

Forskningsinteresser

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

INF113 Innføring i operativsystem

INF100 Innføring i programmering

Vitenskapelig artikkel
  • Vis forfatter(e) (2024). Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages. ACM Transactions on Programming Languages and Systems. 1-58.
  • Vis forfatter(e) (2023). Semantics-Based Version Control for Feature Model Evolution Plans. NIKT: Norsk IKT-konferanse for forskning og utdanning. 14 sider.
  • Vis forfatter(e) (2023). Runtime Enforcement Using Knowledge Bases. Lecture Notes in Computer Science (LNCS). 220-240.
  • Vis forfatter(e) (2023). Modular Soundness Checking of Feature Model Evolution Plans. Lecture Notes in Computer Science (LNCS). 417-437.
  • Vis forfatter(e) (2022). Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins. Lecture Notes in Computer Science (LNCS). 188-204.
  • Vis forfatter(e) (2022). I Can See Clearly Now: Clairvoyant Assertions for Deadlock Checking. Lecture Notes in Computer Science (LNCS). 1-18.
  • Vis forfatter(e) (2020). Behavioral Contracts for Cooperative Scheduling. Lecture Notes in Computer Science (LNCS). 85-121.
  • Vis forfatter(e) (2019). Translating active objects into colored Petri nets for communication analysis. Science of Computer Programming. 1-26.
  • Vis forfatter(e) (2019). Geological Multi-scenario Reasoning. NIKT: Norsk IKT-konferanse for forskning og utdanning. 12 sider.
  • Vis forfatter(e) (2019). Asynchronous Cooperative Contracts for Cooperative Scheduling. Lecture Notes in Computer Science (LNCS). 48-66.
  • Vis forfatter(e) (2018). Program Verification for Exception Handling on Active Objects Using Futures. Lecture Notes in Computer Science (LNCS). 73-88.
  • Vis forfatter(e) (2018). A modular reasoning system using uninterpreted predicates for code reuse. Journal of Logical and Algebraic Methods in Programming. 82-102.
  • Vis forfatter(e) (2017). Translating Active Objects into Colored Petri Nets for Communication Analysis. Lecture Notes in Computer Science (LNCS). 84-99.
  • Vis forfatter(e) (2017). Locally abstract, globally concrete semantics of concurrent programming languages. Lecture Notes in Computer Science (LNCS). 22-43.
  • Vis forfatter(e) (2017). A Survey of Active Object Languages. ACM Computing Surveys. 39 sider.
  • Vis forfatter(e) (2016). Session-based compositional analysis for actor-based languages using futures. Lecture Notes in Computer Science (LNCS). 296-312.
  • Vis forfatter(e) (2015). History-Based Specification and Verification of Scalable Concurrent and Distributed Systems. Lecture Notes in Computer Science (LNCS). 217-233.
  • Vis forfatter(e) (2015). Compositional reasoning about active objects with shared futures. Formal Aspects of Computing. 551-572.
  • Vis forfatter(e) (2014). A sound and complete reasoning system for asynchronous communication with shared futures. Journal of Logic and Algebraic Programming. 360-383.
  • Vis forfatter(e) (2012). Observable behavior of distributed systems: Component reasoning for concurrent objects. Journal of Logic and Algebraic Programming. 227-256.
  • Vis forfatter(e) (2012). Compositional Reasoning about Shared Futures. Lecture Notes in Computer Science (LNCS). 94-108.
  • Vis forfatter(e) (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.
Vitenskapelig foredrag
  • Vis forfatter(e) (2015). KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS.
  • Vis forfatter(e) (2015). A Dynamic Logic with Traces and Coinduction.
  • Vis forfatter(e) (2013). Comparison of Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. In proceedings of NWPT'13.
  • Vis forfatter(e) (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects.
Mastergradsoppgave
  • Vis forfatter(e) (2021). Three-Way Semantic Merge for Feature Model Evolution Plans.
  • Vis forfatter(e) (2021). Modular Soundness Checking of Feature Model Evolution Plans.
Vitenskapelig Kapittel/Artikkel/Konferanseartikkel
  • Vis forfatter(e) (2022). Subsurface Evaluation Through Multi-scenario Reasoning. 31 sider.
  • Vis forfatter(e) (2020). Consistency-Preserving Evolution Planning on Feature Models. 12 sider.
  • Vis forfatter(e) (2014). Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. 8 sider.
  • Vis forfatter(e) (2013). A comparison of runtime assertion checking and theorem proving forconcurrent and distributed systems. 3 sider.
  • Vis forfatter(e) (2012). Soundness of a Reasoning System for Asynchronous Communication with Futures. 3 sider.
  • Vis forfatter(e) (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects. 2 sider.
  • Vis forfatter(e) (2010). Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects. 2 sider.

Se fullstendig oversikt over publikasjoner i CRIStin.

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)

Forskergrupper