Software and System Verification

The lab specializes in the design and application of software engineering techniques based on formal methods for the specification and verification of reliability and security of software systems. The techniques used are applied to the source code, contributing to an improvement of the development process in a secure way (DevSecOps), with a view to quality assurance and certification of software systems.
The laboratory, through its participants, founded the spin-off SecuraFactors, specialized in the security verification of robotic systems, and is an active part of the technology transfer projects of RIR Improvenet.

Research group

Collaborators

  • Souvick Das
  • Raunak Bag
  • Badaruddin Chachar
  • Giacomo Zanatta
  • Giacomo Boldini
  • Teodors Lisovenko
  • Aradhita Mukherjee
  • Vincenzo Arceri (Università di Parma)

Website: ssv.dais.unive.it

Collaborations

Publications

  • Pietro Ferrara, Vincenzo Arceri, Agostino Cortesi: Challenges of software verification: the past, the present, the future. Int. J. Softw. Tools Technol. Transf. 26(4): 421-430 (2024)
  • Giacomo Zanatta, Gianluca Caiazza, Pietro Ferrara, Luca Negrini, Ruffin White Automating ROS2 Security Policies Extraction through Static Analysis , Proceedings of IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) (2024)
  • Luca Olivieri, Luca Negrini, Vincenzo Arceri, Fabio Tagliaferro, Pietro Ferrara, Agostino Cortesi, Fausto Spoto: Information Flow Analysis for Detecting Non-Determinism in Blockchain. ECOOP 2023: 23:1-23:25
  • Mandira Roy, Raunak Bag, Novarun Deb, Agostino Cortesi, Rituparna Chaki, Nabendu Chaki: SCARS: Suturing wounds due to conflicts between non-functional requirements in autonomous and robotic systems. Softw. Pract. Exp. 54(5): 759-795 (2024)
  • Souvick Das, Novarun Deb, Nabendu Chaki, Agostino Cortesi: Driving the Technology Value Stream by Analyzing App Reviews. IEEE Trans. Software Eng. 49(7): 3753-3770 (2023)

Awards

  • The spin-off SecuraFactors won the SmartCup Veneto 2020 for the ICT sector

Research projects

  • Ecodigify (Erasmus+): EcoDigify aims to initiate a future-oriented interdisciplinary university program that will address the multidimensional challenges of promoting sustainability in the use and development of digital technologies. This will be achieved by enhancing the educators’ knowledge about Sustainable Digitalization and providing students with the knowledge
  • SERICS (PNRR Partenariato esteso): SERICS - Security and Rights in CyberSpace is an extended partnership involving several Italian universities and focused on cybersecurity activities. The SSV laboratory is involved in the activity of Spoke 6 about Software and Platform Security. The goal of this spoke is twofold:  (i) provide an ecosystem where software developers can easily reason about software security, and (ii) provide innovative solutions to protect the software supply chain, including the software management and development process.
    Website: https://serics.eu/en/
  • iNEST (PNRR Ecosistemi dell'innovazione): iNEST - Interconnected Nord-Est Innovation Ecosystem is an innovative ecosystem whose model is based on the extensive use of information and communication technologies and digitization, and aims at the development of innovative technologies for people’s well-being and the dissemination of culture and economic and entrepreneurial growth. The SSV lab is involved in the activities of Spoke 3 about "Green and digital transition for advanced manufacturing technology".
    Website: https://www.consorzioinest.it/en/

Families_Share: Socializing and sharing time for work/ life balance through digital and social innovation

The Families_Share Project is financed by the Directorate-General Communications Networks, Content and Technology. It aims to offer a bottom-up solution and a codesigned platform supporting families with sharing time and tasks related tochildcare, parenting, after-school and leisure activities and other household tasks— with a particular focus on low-income families. Seven Families_Share City Labs will be activated in 7 European Cities To achieve this objective, the project will build on current practices which are already leveraging on mutual help and support among families, such as Time Banks, Social Streets, and self-organizing networks of parents active at the neighborhood level and seek to harness the potential of ICT networksand mobile technologies to increase the effectiveness of participatory innovation.

Website: http://www.families-share.eu/
Facebook: https://www.facebook.com/familiesShare/
Twitter: https://twitter.com/Families_Share

EQUAL-IST: Gender Equality Plans for Information Sciences and Technology Research Institutions

The EQUAL-IST Project aims at supporting structural change processes for gender equality in 7 Faculties/Departments of Informatics and Information Systems and Technologies in Finland, Germany, Italy, Lithuania, Portugal, Ukraine. The partner universities will go through a first phase of analysis and internal audit aimed at assessing to what extent gender inequalities / stereotypes are present within human resources management and work organization, decision-making processes, but also research, student services and institutional communication. The data collected will be the subject of an internal discussion open to academic and administrative staff and students, through the use of a crowdsourcing platform that will serve to co-design Action Plans for Gender Equality in each of the institutions involved. The Action Plans will include several interventions that will be tested and monitored in the individual contexts until the closure of the project. Dissemination and networking activities with other Universities in Europe, synergy with Euraxess-HRS4R and development of sustainability scenarios for Action Plans on Gender Equality complete the project.

Website: http://equal-ist.eu/
Facebook: https://www.facebook.com/EQUALISTproject/
Twitter: https://twitter.com/EQUALISTproject

ADditive Manufacturing & INdustry 4.0 as innovation Driver - ADMIN 4D

The ADMIN 4D project involves various enabling technologies in the field of "Smart Manufacturing" intelligent specialization. It is developed through an unprecedented collaboration between leading exponents in the field of research and industrial implementation of the different technologies involved: additive technology (known as 3D printing), materials engineering, sensors in the environment of Internet of Things and mechanics/mechatronics.
The goal of the project is the development of an innovative system for the collection and processing - through the use of ad hoc algorithms - of technical-chemical information from the new materials and binders used in the products and from the production equipment (3D printing) patented by the project partners and still subject to R&D activities aimed at their improvement and diffusion in the territories.

VIR2EM - VIrtualization and Remotization for Resilient and Efficient Manufacturing

The VIR2EM project (VIrtualization and Remotization for Resilient and Efficient Manufacturing), proposes to use virtualization technologies for processes, systems, and resources to foster remote operations in Industrial Networks.In the context of Smart Manufacturing, Software and infrastructural solutions for the Internet of Things are in eager need of analysis and development of fundamental aspects associated with cybersecurity and improvement to the usability, and the impact on business models and organizations, to the application of techniques from the Information Technology (IT) world to the specific field of Operation Technology (OT).
The goals of the project include:
(i) maximize the efficiency of production systems under normal operating conditions,
(ii) maintain operations in the event of emergencies,
(iii) ease the restart of operations downstream of emergencies, guaranteeing flexibility and predictive capacity.
To do that, the project aims, among other things, to the development of monitoring tools, remote control supervision, and optimization of service and after-sales operations, with a focus on
(i) interpretable methodologies,
(ii) methodologies for the fog computing scenario,
(iii) "lifelong learning" approaches.

MIUR-MAE Italy-India - Formal Specifications for Safe Software Systems

The aim of the project is to investigate whether the security policies of critical software systems can be formally integrated into requirements specification techniques using formal methods, to identify ambiguities and inconsistencies already during the specification phase of the software life cycle. To this end, we will apply lightweight validation and verification techniques to "secure" the software already in the requirements engineering phase. In particular, we will apply modeling languages such as Event-B and iSTAR to specify and analyze the requirements so that the software design can comply with safety criteria. Overall, the project responds to the need to use mathematical techniques with a solid theoretical foundation to validate security aspects of software applications.

Last update: 04/11/2024