Department of Information Technology

Automated Reasoning Arena

To promote multidisciplinary collaboration between divisions and between the Department of Information Technology and external parts.

Current Research Activities within the Arena

String Solvers

Most SMT and CP solvers are currently limited to the theories of integers and arrays. However, string data types are present in all conventional programming and scripting languages. In fact, it is impossible to capture the essence of many programs, for instance in database and web applications, without the ability to precisely represent and reason about string data types. The control flow of programs can depend on the words denoted by the string variables, on their lengths, or on the regular languages to which they belong. For example, a program allowing users to choose a username and a password may require the password to be of a minimal length, to be different from the username, and to be free from invalid characters. Reasoning about such constraints is also crucial when verifying that database and web applications are free from SQL injections and other security vulnerabilities.

This project intends to design decision procedures for the string data type. Furthermore, this project will try to develop methods for integrating string solvers with other theories, explore different Craig interpolation techniques, and explore the applicability of the developed framework to general classes of programs.

Contact: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Pierre Flener, Justin Pearson, and Philipp Rümmer

Constraint Programming (CP)

See the CP research on global constraints, constraint-based local search, symmetry in models and search, constraint-based modelling, and analysis, testing, and verification of the Optimisation Group.

Contact: Pierre Flener and Justin Pearson

Contact Us

The Automated Reasoning Arena is part of the Department of Information Technology and is situated at the Information Technology Center (ITC) in Uppsala, Sweden.

Arena coordinator
Mohamed Faouzi Atig
More Contacts
Philipp Rümmer (Division of Computer Systems)
Tjark Weber (Computing Science Division)

Automated Reasoning Arena e-mail list
To subscribe to the list, send a message to with the following text in the body of the message:

subscribe it-AutomatedReasoning <My Name>

The list will be used for announcements. You can reach the moderators of the list by sending a message to

Updates
  • Kick-off meeting: 28 March 2018
Updated  2018-08-15 10:56:53 by Mohamed Faouzi Atig.