Home
Crystal Chang Din's picture

Crystal Chang Din

Associate Professor
  • E-mailCrystal.Din@uib.no
  • Phone+47 944 83 808
  • Visitor Address
    HIB - Thormøhlens gate 55
  • Postal Address
    Postboks 7803
    5020 Bergen

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

I am a member of ECOOP 2021 Artifact Evaluation Committee and UDIT 2021 Program Committee.

 

Available master thesis topics:

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)

INF113 Introduction to Operating Systems

Academic article
  • Show author(s) 2020. Behavioral Contracts for Cooperative Scheduling. Lecture Notes in Computer Science (LNCS). 85-121.
  • Show author(s) 2019. Translating active objects into colored Petri nets for communication analysis. Science of Computer Programming. 1-26.
  • Show author(s) 2019. Geological Multi-scenario Reasoning. NIKT: Norsk IKT-konferanse for forskning og utdanning. 12 pages.
  • Show author(s) 2019. Asynchronous Cooperative Contracts for Cooperative Scheduling. Lecture Notes in Computer Science (LNCS). 48-66.
  • Show author(s) 2018. Program Verification for Exception Handling on Active Objects Using Futures. Lecture Notes in Computer Science (LNCS). 73-88.
  • Show author(s) 2018. A modular reasoning system using uninterpreted predicates for code reuse. Journal of Logical and Algebraic Methods in Programming. 82-102.
  • Show author(s) 2017. Translating Active Objects into Colored Petri Nets for Communication Analysis. Lecture Notes in Computer Science (LNCS). 84-99.
  • Show author(s) 2017. Locally abstract, globally concrete semantics of concurrent programming languages. Lecture Notes in Computer Science (LNCS). 22-43.
  • Show author(s) 2017. A Survey of Active Object Languages. ACM Computing Surveys. 39 pages.
  • Show author(s) 2016. Session-based compositional analysis for actor-based languages using futures. Lecture Notes in Computer Science (LNCS). 296-312.
  • Show author(s) 2015. History-Based Specification and Verification of Scalable Concurrent and Distributed Systems. Lecture Notes in Computer Science (LNCS). 217-233.
  • Show author(s) 2015. Compositional reasoning about active objects with shared futures. Formal Aspects of Computing. 551-572.
  • Show author(s) 2014. A sound and complete reasoning system for asynchronous communication with shared futures. Journal of Logic and Algebraic Programming. 360-383.
  • Show author(s) 2012. Observable behavior of distributed systems: Component reasoning for concurrent objects. Journal of Logic and Algebraic Programming. 227-256.
  • Show author(s) 2012. Compositional Reasoning about Shared Futures. Lecture Notes in Computer Science (LNCS). 94-108.
  • Show author(s) 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.
Academic lecture
  • Show author(s) 2015. KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS.
  • Show author(s) 2015. A Dynamic Logic with Traces and Coinduction.
  • Show author(s) 2013. Comparison of Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. In proceedings of NWPT'13.
  • Show author(s) 2010. Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects.
Masters thesis
  • Show author(s) 2021. Three-Way Semantic Merge for Feature Model Evolution Plans.
  • Show author(s) 2021. Modular Soundness Checking of Feature Model Evolution Plans.
Academic chapter/article/Conference paper
  • Show author(s) 2020. Consistency-Preserving Evolution Planning on Feature Models. 12 pages.
  • Show author(s) 2014. Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. 8 pages.
  • Show author(s) 2013. A comparison of runtime assertion checking and theorem proving forconcurrent and distributed systems. 3 pages.
  • Show author(s) 2012. Soundness of a Reasoning System for Asynchronous Communication with Futures. 3 pages.
  • Show author(s) 2010. Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects. 2 pages.
  • Show author(s) 2010. Observable Behavior of Dynamic Systems: Component Reasoning for Concurrenct Objects. 2 pages.

More information in national current research information system (CRIStin)