Reliable Software Evolution Project

This project aims to combine testing techniques and formal methods in order to improve the reliability of evolving software. Focusing on software evolution allows us to deal with an important phase in the life cycle of software systems, and leverage the incremental nature of change. The complementary strengths of testing techniques and formal methods can help to achieve precision and scalability.

The increasing complexity of software systems, and the growing reliance on computers and software, makes it ever more important to ensure that the software operates without failure, especially in safety critical systems. Building software with high quality from the beginning of its life-cycle is crucial, but not sufficient, since the software evolves during its development and after its release in response to changing  user needs and environments.

The combination of software verification and testing techniques is increasingly encouraged due to their complementary strengths, and the different ways to analyze the system --- dynamic (runtime-based) and  static (symbolic), respectively. We have already exploited this combination, and the complementary nature of our research teams' expertise, in our previous work.

The goal of this research proposal is to increase the reliability of evolving software by advancing research in two directions:
(1) combining formal methods with regression testing techniques, by  enhancing verification-based regression testing of individual methods and method call sequences, and (2) combining formal verification with slicing and partial evaluation techniques, by using slicing and partial evaluation to simplify verification.

The project is planned over three years and approved by the German Israeli Foundation (GIF) .