•  I
• a · A  I
• Accesibility  I
• Map  I
• Search  I
• Staff directory

• ::  Iniciar sessió :: 

The absence of errors is the great chimera of the software industry. Considering the weight that computing is taking in today's society, from the apps we use on our mobiles to critical sectors such as traffic control or banking transactions, guaranteeing the absence of errors in the software is increasingly necessary.

With this objective in mind, a team from the Universitat Politècnica de València (UPV), belonging to the Valencian Institute of Artificial Intelligence (VRAIN), is participating in EuroProofNet, a European research network on digital testing whose aim is to contribute to achieving error-free software. Its implementation is part of a COST (European Cooperation in Science and Technology) action on formal proofs that aims to place Europe at the forefront of leadership in formal verification.

As Alicia Villanueva, a researcher at the UPV's VRAIN Institute, points out, nowadays there exists very secure software that undergoes very demanding formal analysis and verification processes. When the smallest failure can cause major human, material or economic disasters these proofs are key. And today this is true at all levels.

"For example, we are sometimes unaware of the importance of having our mobile apps verified. Many of them manage our data, our accounts, so any vulnerability can affect both users and the developers themselves. That is why it is important to try to make progress not only in the development of the techniques themselves, but also in making the verification tools more accessible. Nowadays, it is not only critical the software for aeronautical and railway control systems, etc., which are developed with budgets in the millions and for which we have already accepted the need to guarantee their correctness. By making formal verification tools more usable, we can help improve the safety and quality of any software system," says Villanueva.

The UPV, at the forefront of software verification research

The network has more than 200 researchers from 30 countries, both within and outside the European Union, and includes six working groups, each specialising in a specific area. The VRAIN-UPV team leads the group working on program verification.

"In this group, what we are trying to improve are formal verification techniques that in turn make use of formal proof systems. The main characteristic of formal verification is that it can guarantee that a property is fulfilled for any possible execution, thus contributing to the security of the software," explains Alicia Villanueva.

Although a multitude of effective verification tools exist today, they are often specialised in solving a specific type of problem. In this context, EuroProofNet has two main objectives: on the one hand, to improve the interoperability and usability of formal proof systems, thus contributing to the advancement of the verification tools that make use of them, and on the other hand, to improve interoperability between verification systems in order to take advantage of the best of each technique. "All of this will contribute to ensuring the security of software," says Alicia Villanueva.

In addition to the purely scientific objectives, EuroProofNet aims to build a network of researchers that will foster collaboration and help to make progress in this area. The network will be active until October 2025.