Eight new projects at CSE funded by the Swedish Research Council

Eight researchers at the department of Computer Science and Engineering were awarded grants by the Swedish Research Council within the Natural and engineering sciences 2019 call.
"We are very pleased to see that our research is top notch in such a wide range, from computer architecture to type theory, from smart contracts to AI.” says Patrik Johansson, Deputy Head of Department at Computer Science and Engineering at Chalmers and University of Gothenburg.

Smart Contract Verification

Wolfgang Ahrendt is a professor in the Formal Methods division.
Wolfgang Ahrendt
Blockchain is an open infrastructure in the internet that records transactions between parties which do not trust each other, without relying on any central authority. The most famous application of blockchain is cryptocurrencies like Bitcoin. Another one is 'smart contracts', which are programs automating the exchange of cryptocurrencies and information between parties. If there is any error in the programming of a smart contract, the error can be exploited by malicious users, causing substantial financial damage, in some cases millions of Dollars. 
In this project, we will develop methods to verify, with mathematical certainty, whether a smart contract is free of errors. The outcome of the project will contribute to the safety of the arising digital market places.
Funding: 4 year project grant, total of 4 million SEK.

Information, Fairness and Socially Beneficial Artificial Intelligence

Christos Dimitrakakis is a docent in the Data Science and AI division. To read more about fairness in artificial intelligence, visit this page.
Christos Dimitrakakis
Artificially intelligent (AI) systems are playing an ever increasing role in society. To ensure that they are beneficial, we must guarantee that they act not only according to the designer's intentions, but also in a way that is fair to all individuals and groups affected by their decisions. Many applications integrate human and AI decisions, such as crowdsourcing, recommendation systems, navigation and autonomous vehicles, as well as decision support systems for credit risk and criminal recidivism. AI systems are also deployed in semi-automated design tools, and diagnostics in medicine. Humans interact with a pre-designed AI, which may be unaware of the motivations, behaviour or knowledge of people. When such an AI is used at scale, it must take into account broader, societal considerations, such as fairness and privacy. Our project will create algorithms for automatically aligning AI behaviour with societal values.
Funding: 4 year project grant, total of 4 million SEK.

Context-Infused Automated Software Test Generation

Gregory Gay is a senior lecturer in the Software Engineering division. More information about his research is available at http://greggay.com/
Gregory Gay Software testing is invaluable in ensuring reliability. It is also difficult and expensive, with serious consequences. Automation is critical in controlling costs and focusing developers. A promising avenue of automation is search-based test generation – the framing of tasks such as input selection as optimization problems. However, current approaches to search-based generation fail to match the effectiveness of human developers because of the use of naive universal strategies to guide input selection. Developers are driven by context – domain, requirements, and past experience. Effective automated test generation requires this context to control "how" code is executed. The next generation of test generation tools must be multi-objective, incorporate domain-specific information, and be adaptable to the system under test. I propose two families of context-infused strategies and a new self-adaptive generation approach that can customize its selection of strategies. These research advances should yield more "human-like" – and human-competitive – results.
Funding: 4 year starting grant, total of 3,9 million SEK.

Non-Functional Requirements for Machine Learning: Facilitating Continuous Quality Awareness (iNFoRM)

Jennifer Horkoff is an associate professor in the Software Engineering division.
Jennifer Horkoff
Machine Learning (ML) uses big data to enable software algorithms to “learn”, solving difficult problems such as recognizing images and diagnosing cancer. Software Engineering (SE) focuses on understanding, decomposing, managing, formalizing and reasoning over software qualities (e.g., performance, reliability, security, maintainability, usability), also called non-functional requirements (NFRs). 
From an SE perspective, the meaning of certain qualities, how to refine those qualities, and how to use such qualities for design and run time decision making is relatively well established and understood. However, in a context where the solution involves ML, much of our knowledge about NFRs no longer applies. E.g., what does it mean for a ML enabled system to be maintainable, modifiable and testable? How are these qualities measured for an ML solution? Are NFRs such as compatibility and modularity still relevant for ML solutions? Furthermore, new NFRs such as fairness and transparency have become critical from an ML perspective, including knowledge of new NFR tradeoffs, e.g., fairness vs. accuracy.
The overall objective of the project is to create a framework to define, decompose, express, monitor, and reason (make tradeoffs) over NFRs for systems involving ML, accounting for the uniqueness of ML solutions compared to typical software.
Funding: 4 year project grant, total of 4 million SEK.

X-LEGAL: smart legal contracts

Gerardo Schneider is a professor in the Formal Methods division.
This project aims at legal automation, by integrating two notions of "contracts": legal contracts, i.e., legally binding normative documents establishing mutual agreements between competent and freely participating parties, and "smart contracts", computer programs executed in the blockchain. The problem today is that smart contracts are not "smart" nor "contracts". The dream of executable legal contracts is still not a reality but a desirable outcome on blockchain technologies. We will bridge this gap by proposing two languages: one closer to the non-technical users having an explicit and clear presentation of the contractual clauses, the other one closer to executable code but still in connection with the contractual language.
Funding: 4 year project grant, total of 4 million SEK.

PRIME: Memory that can compute on stored data. 

Per Stenström is a professor in the Computer Engineering division.
In today’s computers, most of the time is spent by the central processing unit (CPU) bringing the data from memory, performing the operations and sending the result back to memory. Such systems become very inefficient due to costly data transfers specially for modern applications such as Machine Learning and Big Data analytics, which perform many operations on large amounts of data stored in memory. 
With this project we exploit adding computation capabilities to the memory so that operations can be performed where the data is stored, thus eliminating the inefficient data transfers. We will develop a new computational model in which code move around instead of data, which is more inefficient. This will yield computer systems with substantially higher processing rates and lower energy consumption.
Funding: 4 year project grant, total of 4 million SEK.

Also granted

Modal type theory with dependent types

Andreas Abel, senior lecturer in the Logic and Types division.
Funding: 4 year project grant, total of 4 million SEK.

Evidence theory and semantics for homotope theory in higher order categories

Christian Sattler, Logic and Types division.
Funding: 4 year starting grant, total of 3,9 million SEK.

Published: Wed 27 Nov 2019.