Software and System Verification
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/848x174/banner_SeSV_848x174.jpg)
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.
Collaborators
- Raunak Bag
- Gianluca Caiazza
- Luca Negrini
- Martina Olliaro
- Maikel Lazaro Perez Gort
- Alvise Spanò
- Ruffin White
Website: ssv.dais.unive.it
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/Lab_SeSV_600x362.jpg)
Collaborations
- Ecole Normale Superieure Paris
- ETH Zurich
- University of Calcutta
- University of Patna
- Meta
- Università di Verona
- Università di Padova
- Università di Cagliari
Publications
- Vincenzo Arceri, Martina Olliaro, Agostino Cortesi, Isabella Mastroeni: Completeness of string analysis for dynamic languages. Information and Computation 281: 104791 (2021)
- Pietro Ferrara, Amit Kr Mandal, Agostino Cortesi, Fausto Spoto: Static analysis for discovering IoT vulnerabilities. Int. J. Softw. Tools Technol. Transf. 23(1): 71-88 (2021)
- Maikel Lázaro Pérez Gort, Martina Olliaro, Agostino Cortesi, Claudia Feregrino Uribe: Semantic-driven watermarking of relational textual databases. Expert Systems with Application 167: 114013 (2021)
- Angshuman Jana, Raju Halder, Kalahasti Venkata Abhishekh, Sanjeevini Devi Ganni, Agostino Cortesi: Extending Abstract Interpretation to Dependency Analysis of Database Applications. IEEE Transactions on Software Engineering 46(5): 463-494 (2020)
- Pietro Ferrara, Agostino Cortesi, Fausto Spoto: From CIL to Java bytecode: Semantics-based translation for static analysis leveraging. Sci. Comput. Program. 191: 102392 (2020)
- Ruffin White, Gianluca Caiazza, Agostino Cortesi, Young Im Cho, Henrik I. Christensen: Black Block Recorder: Immutable Black Box Logging for Robots via Blockchain. IEEE Robotics Automation Letters 4(4): 3812-3819 (2019)
Awards
- The spin-off SecuraFactors won the SmartCup Veneto 2020 for the ICT sector
Research projects
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/Families_Share_600x362.jpg)
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
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/EQUAL-IST_600x362.jpg)
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
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/ADMIIN-4D_600x362.jpg)
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.
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/VIR2EM_600x362.jpg)
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.
![](/pag/fileadmin/user_upload/dipartimenti/DAIS/img/600x362/Specifiche_Formali_600x362.jpg)
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: 28/08/2024