Research Programs

Software Engineering and Formal methods


Our goal is to develop languages, methods, techniques and tools to support the design and deployment of trustworthy and effective software systems.

Research Areas

Goal-Oriented Requirements Engineering studies methods and techniques to model and analyze not only traditional functional and non-functional requirements for a software system, but also questions concerning why, by whom, and when these requirements are needed.  It well characterizes complex systems where humans and software systems interacts.

Agent-Oriented Software Engineering proposes methodologies for building software that are founded on the concept of agent and related mentalistic and social notions. This research area covers all phases of software development, including requirements, architectural and detailed design, as well as implementation, using agent-oriented infrastructures .

Security Engineering is the dual discipline of software engineering and focuses on the design of secure systems, It identifies methods and tools for incorporating security concerns from the early phases of the system design, taking into account notion such as trust relationships, attacker models, and risk analysis. It builds on formal methods in order to provide verifiable assurance.

Security-by-Contract proposes new models and practical enforcement mechanisms to guarantee the compliance of applications and services to the security policies dictated by users or regulators. It provides mobile code and distributed services with the notion of security contracts and key assurance indicators that can be designed, verified at deployment time and enforced during execution.

Formal Methods are powerful techniques for specifying and verifying complex systems (SW, HW, Protocols). In particular, model checking is currently one of the most popular and effective formal verification techniques, which exploits the dramatic efficiency of current state-of-the-art satisfiability solvers workhorse power. We work on developing novel and effective techniques for model checking and satisfiability for industrial scale formal methods.

Applications Areas

Results from our research have been applied to software development, software/protocols/hardware verification, service-oriented architecture design and development, organizational and business process modeling and analysis, and mobile software systems development.


Together with Univ. of Toronto,we have invented the Tropos design methodology that has introduced innovative modeling and analysis techniques for capturing requirements and developing software. We have developed a CASE tool supporting a number of techniques to analyze requirements, automatically generate possible designs, and reason about security and risk ( We are one of the research group (with FBK, Univ. of Genova and CMU) behind the world state of the art NuSMV model checker ( and  (with FBK) of the MathSAT SMT solver ( Which is currently used by Intel as a back-end workhorse solver  in a joint project. The research results of the S3MS project on Security-by-Contract for mobile code ( that integrates security monitors and securoity verification technology (MathSAT) on a mobile device have been selected by the EU for publication in ICT Results on Cordis and the project has further decide to protect the results under the SxC trademark.

We coordinate 2 EU project (S3MS and SecureChange), scientifically lead another IP  (MASTER),  and participate in a third one (SERENITY);for two years we have been the recipient of an industry grant by Intel for a total grant amount of over 8M€.

We have the following major projects:

  • EU-FP7-IST-IP-SecureChange 2009-2011-Security Engineering for lifelong Evolvable System - (EU Administrative Coordinator)  funding 5.1M€
  • EU-FP7-IST-IP-MASTER 2008-2010- Managing Assurance, Security and Trust for Services - (EU Scientific Coordinator)  funding 920K€
  • EU-FP6- IST-STREP S3MS 2006-2008 of Software and Services for Mobile Systems (EU Admin Coordinator) -funding 2.4M€
  • EU-FP6- IST-IP SERENITY 2006-08 and Dependability Engineering - funding 586K€
  • PAT-FU-MOSTRO 2004-2007 - Modelling Security and Trust Relationships within Organizations - funding 81K€
  • MIUR-FIRB 2004-2006 - Automatic Verification of Internet Security Protocols - funding 92K€
  • MIUR-PRIN 2008-2010 - Integrating automated reasoning in model checking - funding  35K€
  • Intel-INDUSTRY 2009-2011 - Word-level Formal Verification via SMT Solving - funding 180K USD



Faculty Members

Paolo GiorginiRoberto Sebastiani (Coord)

Further Information

Technical reports of Research Program
Published papers of Research Program