The Department of Computer Science and Engineering is joint between Chalmers and the University of Gothenburg, where the university part is included in the IT Faculty.

More information: Computer Science and Engineering

Collections in this community

Recent Submissions

  • A Survey on Satisfiability Checking for the μ -Calculus Through Tree Automata 

    Hausmann, Daniel; Piterman, Nir (2022)
    Algorithms for model checking and satisfiability of the modal μ -calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and ...
  • Automated replication of tuple spaces via static analysis 

    De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Uwimbabazi, Aline (2022)
    Coordination languages for tuple spaces can offer significant advantages in the specification and implementation of distributed systems, but often do require manual programming effort to ensure consistency. We propose an ...
  • Modelling Flocks of Birds from the Bottom Up 

    De Nicola, Rocco; Di Stefano, Luca; Inverso, Omar; Valiani, Serenella (2022)
    We argue that compositional specification based on formal languages can facilitate the modelling of, and reasoning about, sophisticated collective behaviour in many natural systems. One defines a system in terms of individual ...
  • A PO Characterisation of Reconfiguration 

    Abd Alrahman, Yehia; Martel, Mauricio; Piterman, Nir (2022)
    We consider partial order semantics of concurrent systems in which local reconfigurations may have global side effects. That is, local changes happening to an entity may block or unblock events relating to others, namely, ...
  • On the Specification and Monitoring of Timed Normative Systems 

    Azzopardi, Shaun; Pace, Gordon J.; Schapachnik, Fernando; Schneider, Gerardo (2022)
    In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily ...
  • Runtime Verification of Kotlin Coroutines 

    Furian, Denis; Azzopardi, Shaun; Falcone, Yliès (2022)
    Kotlin was introduced to Android as the recommended language for development. One of the unique functionalities of Kotlin is that of coroutines, which are lightweight tasks that can run concurrently inside threads. Programming ...
  • AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification 

    Azzopardi, Shaun; Ellul, Joshua; Falzon, Ryan; Pace, Gordon J. (International Conference on Runtime Verification, 2022)
    Aspect-oriented programming tools aim to provide increased code modularity by enabling programming of cross-cutting concerns separate from the main body of code. Since the inception of runtime verification, aspect-oriented ...
  • Tainting in Smart Contracts: Combining Static and Runtime Verification 

    Azzopardi, Shaun; Ellul, Joshua; Falzon, Ryan; Pace, Gordon J. (Lecture Notes in Computer Science book series (LNCS,volume 13498), 2022)
    Smart contracts exist immutably on blockchains, making their pre-deployment correctness essential. Moreover, they exist openly on blockchains—open for interaction with any other smart contract and offchain entity. Interaction, ...
  • Model Checking Reconfigurable Interacting Systems 

    Alrahman, Yehia Abd; Azzopardi, Shaun; Piterman, Nir (International Symposium on Leveraging Applications of Formal Methods, 2022)
    Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming ...
  • Runtime Verification meets Controller Synthesis 

    Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo (2022)
    Reactive synthesis guarantees correct-by-construction controllers from logical specifications, but is costly—2EXPTIME-complete in the size of the specification. In a practical setting, the desired controllers need to ...
  • R-CHECK: A Model Checker for Verifying Reconfigurable MAS 

    Alrahman, Yehia Abd; Azzopardi, Shaun; Piterman, Nir (AAMAS 2022, 2022)
    Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by ...
  • Incorporating Monitors in Reactive Synthesis without Paying the Price 

    Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo (19th International Symposium on Automated Technology for Verification and Analysis, 2021)
    Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative speci cations, and have found ...
  • Groupoid-Valued Presheaf Models of Univalent Type Theory 

    Ruch, Fabian (2022-11-03)
    One main goal of this thesis is to study constructive models of type theory with one univalent universe that interpret types by “presheaves” of groupoids. A starting point is the fact that the groupoid model can be ...
  • Facilitating Feature-Oriented Quality Assurance in Low-Maturity Variant-rich Systems 

    Mukelabai, Mukelabai (2022-09-08)
    Context: Many software systems exist in several variants customized for specific stakeholder requirements, such as different market segments or hardware constraints. This customization introduces a high level of complexity ...
  • Actions over Core-closed Knowledge Bases 

    Cauli, Claudia; Ortiz, Magdalena; Piterman, Nir (2022)
    We present new results on the application of semantic- and knowledge-based reasoning techniques to the analysis of cloud deployments. In particular, to the security of Infrastructure as Code configuration files, encoded ...
  • Pre-deployment Description Logic-based Reasoning for Cloud Infrastructure Security 

    Cauli, Claudia (2022-05-25)
    Ensuring the security of a cloud application is exceptionally challenging. Not only is cloud infrastructure inherently complex, but also a precise definition of what is secure is hard to give. Business context, regulatory ...
  • Generative comics - A computational approach to creating comics material 

    Nairat, Malik (2021-09-24)
    Digital storytelling can be employed as a tool that incorporates human creativity with technology. It synthesizes multimedia based elements to create engaging stories and compelling narratives. To this end, this research ...
  • Service Robotics Software Engineering 

    García, Sergio (2021-08-16)
    Context. Robots are increasingly becoming involved in our lives and currently, teams of service robots cooperate to support humans by performing useful, repetitive, or dangerous tasks. However, engineering the robots’ ...
  • Efficiency and Automation in Threat Analysis of Software Systems 

    Katja, Tuma (2020-12-04)
    Context: Security is a growing concern in many organizations. Industries developing software systems plan for security early-on to minimize expensive code refactorings after deployment. In the design phase, teams of experts ...
  • Learning Language (with) Grammars: From Teaching Latin to Learning Domain-Specific Grammars 

    Lange, Herbert (2020-08-25)
    This thesis describes work in three areas: grammar engineering, computer-assisted language learning and grammar learning. These three parts are connected by the concept of a grammar-based language learning application. Two ...

View more