Subventions et des contributions :

Subvention ou bourse octroyée s'appliquant à plus d'un exercice financier. (2017-2018 à 2022-2023)

Modern software systems are incredibly complex engineered artifacts. They rely on intricate algorithms, developed by large, often distributed, teams, and are build out of many interconnected components. Software systems are extremely difficult to get right, to verify, and to certify. Software bugs are common even in such safety-critical industries as medical devices, automotive, and avionics. Yet, our society is increasingly becoming dependent on reliable operation of such systems. The border between safety- and non-safety-critical system is being eroded.

Dealing with this complexity requires increased automation in verification and certification. Since the establishment of the Computer Science discipline, scientists have envisioned a mechanical verifier that would provide this automation. While the last few decades have seen tremendous progress towards this goal, it remains unrealized and challenging task. The long term objective of my proposed research is to develop scalable automated verification that is usable by software engineers and is integrated into the software development lifecycle.

In the next five years, the proposed research will focus on building foundations of scalable automated verification based on Software Model Checking and exploring novel applications of verification in Software Engineering. Particular emphasis will be placed on automating modular reasoning, synthesis of environment assumptions, extending applicability of automated reasoning to complex models, and verification of concurrent and distributed systems. The proposed research will significantly extend applicability and usability of automated verification in practice.

The long-term goal of the proposed research is to develop useful powerful software verification tools and supporting methodologies. These techniques will have a significant impact on Canadian industry by providing tools that will increase confidence and reduce bugs in software systems. Furthermore, the program will train Highly Qualified Personnel with the necessary skills to effectively apply automated verification to software systems.

The research in software verification is highly interdisciplinary, requiring in-depth knowledge of logic, formal methods, automated reasoning, and software engineering. Techniques, decision engines, and tools developed for verification are often applicable to many related problems in Software Engineering and Computer Science. The project will train Highly Qualified Personnel in the fields of Software Verification and Software Engineering with a unique combination of interdisciplinary skills. It is expected that these skills will help the HQP to make a long lasting impact on Canadian industry and research.