Current Research Activities within the Arena
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.
Constraint Programming (CP)
- Arena coordinator
- Mohamed Faouzi Atig
- More Contacts
- Philipp Rümmer (Division of Computer Systems)
- Tjark Weber (Computing Science Division)
subscribe it-AutomatedReasoning <My Name>
- Kick-off meeting: 28 March 2018