The Automated Software Engineering Research Group

Description

The Automated Software Engineering Research Group aims at the development of cutting-edge automated reasoning techniques and their use to build a new generation of push-button software verification and debugging tools supporting the development of complex, large-scale, distributed IT applications.

Publications (click here for the complete list)

• A. Armando, R. Carbone, L. Compagna, J. Cuellar and L. Tobarra. Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. The 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), October 27th, 2008, Hilton Alexandria Mark Center, Virginia, USA.
• A. Armando, J. Mantovani and L. Platania. Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers. To appear on the International Journal on Software Tools for Technology Transfer (STTT),
• A. Armando, M. Benerecetti, D. Carotenuto, J. Mantovani and P. Spica. The Eureka Tool for Software Model Checking. In the proceedings of the 22nd IEEE/ACM ASE Conference, November 5-9, 2007, Atlanta, Georgia, USA.
• A. Armando and L. Compagna. SAT-based Model Checking for Security Protocols Analysis. International Journal of Information Security, vol. 7, no. 1. January 2008.
• A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. New results on rewrite-based satisfiability procedures. To appear on the ACM Transactions on Computational Logic (TOCL).

Fundings (click here for the complete list)

• Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems. (20079E5KM8) funded by the Italian Ministry of Scientific and Technological Research in the context of the PRIN'07 programme. Duration: 24 months from September 20, 2008.
• AVANTSSAR: Automated Validation of Trust and Security of Service-oriented Architectures, STREP project number 216471, funded by the EU in the context of the 7th Framework Programme, THEME ICT-1-1.4 - Secure, dependable and trusted Infrastructures. Duration: 36 months, from January 1, 2008.
• IST FET Open Project AVISPA: Automated Validation of Internet Security Protocols and Applications (IST-2001-39252) funded by the European Commission in the context of the 5th Framework Programme. Partner Institutions: DIST, U. of Genova (Prof. A. Armando, coordinator); Eidgenoessische Technische Hochschule Zurich, ETHZ, Switzerland; INRIA Lorraine, France; Siemens AG, Munich, Germany. Duration: 30 months, from January 1, 2003. In 2006 the AVISPA Project received the nomination for the Descartes Prize for excellence in scientific collaborative research.
• Verifica automatica dei protocolli di sicurezza (RBAU01P5SS) funded by the Italian Ministry of Scientific and Technological Research in the context of the FIRB programme 2001. Partner Institutions: DIST, U. of Genova (Prof. A. Armando, coordinator); U. of Trento; U. of Napoli. Duration: 36 months, from July 1st, 2003.
• Decision Procedures for Software Model Checking (2003097383-002) funded by the Italian Ministry of Scientific and Technological Research in the context of the PRIN'03 programme. Duration: 24 months from November 1, 2003.