We are living in a world that is increasingly run by software. Daily activities, such as online banking, mobile communications and air traffic use, are controlled by software. This software is growing in size and functionality, but its reliability is hardly improving. We are getting used to the fact that computer systems are error-prone and insecure. To (re)gain the trust of end-users in software and Web services, formal automated reasoning is one of the main investments made by ICT companies in preventing software errors.

In this talk I will present recent advancement in automated reasoning, in particular computer-supported theorem proving, for generating and proving software properties that prevent programmers from introducing errors while making changes in this software. When testing programs manipulating the computer memory, our initial results show our work is able to prove that over 80% of test cases are guaranteed to have the expected behavior. The work described in this talk, and its results,
are supported by an ERC Starting Grant and ERC Proof of Concept Grant, aiming at providing ICT customers and investors a tool-supported methodology for ensuring continuous growth in software functionality, thus increasing software reliability and user's trust in software technologies.