The R+D Group MiST
(MultI-paradigm Software Technology)
(Computer assisted validation by using sound and rigorous methods)
January 1, 2014 - December 31, 2016 (3 years)
The main goal of the CAVI-SUM project is helping to make the Spanish software development industry more competitive: (1) by contributing to the advance of the research on software validation based on sound and rigorous techniques and (2) by ensuring its transfer to the industry by developing tools that apply these techniques to solve the current challenges of the software industry.
We live in a digital society in which the software reliability has become a crucial aspect, both because the risks for human lives that a software bug may cause and also for its associated economic cost. Most current software products use heterogenous technologies and different programming languages that are glued together by means of complex mechanisms. This complexity, together with the fact that most software components are made by third-party developers, makes the software validation tasks a true challenge for software development companies in terms of cost. However, validation tasks are crucial for guaranteeing the quality of their products. Therefore, we propose the present R+D project, whose generic goals aim at advancing the knowledge and technology within the area of software validation at different levels:
Software testing. This is the technology most commonly used by the software industry to prevent errors during the software development. The controlled execution of a number of tests allows one to validate, to some extent, the correctness of the software developed. In this project, we will focus on automated techniques for test-case generation.
Formal verification. The main drawback of the previous technique is that, despite the fact that they can be very helpful to locate the bugs of a program, they cannot be used to ensure that a program is error-free. Therefore, we will also consider formal verification techniques that finitely approximate (by means of static analysis, abstract interpretation, constraints, etc.) the possible executions of a program. Thus, we may obtain a total assurance of the correctness of a program, which makes these techniques specially adequate for validating critical software.
Program debugging. Complementary to the previous methods, we can also find a number of debugging techniques that help the programmer to detect and locate the most common program errors. In this project, we will focus on some of the most advanced techniques, namely algorithmic debugging and program slicing.
Besides a number of scientific publications that will help us to disseminate our main achievements, we also plan to develop methods and software tools useful to improve the quality and productivity of the software development process. Therefore, the deliverables of this project will allow us to increase the international visibility of the Spanish research and will also allow the Spanish software development industry to improve its competitiveness by using the most advanced techniques for software validation.
Software, automated validation, formal verification, static analysis, debugging, test case generation, programming languages.