You are here

Formal Methods in Software Engineering

Video about the course (2020/21, in Portuguese) : please see

Current: 2020/21 (Wiki).

Past years:2019/20, 2018/19, 2017/18, 2016/17, 2015/16, 2014/15, 2013/14, 2012/13, 2011/12, 2010/11, 2009/10, 2008/09, 2007/08, 2006/07 or earlier.

As of academic year 2014/15, Formal Methods in Software Engineering (MFES) became a 25 ECTS specialization option proposed by HASLab (High Assurance Software Lab). This option consolidates an experience of three decades in the teaching of formal methods applied to the development of software.

The courses that make up this option,

address core competencies for a truly reliable software application engineering. The option also shares the curricular unit Computer Engineering Laboratory (2nd semester, 10 ECTS (Wiki)) where the knowledge acquired in the core courses is applied in projects proposed by industry partners.

In its theoretical facet, the vision is to approach software problems from an authentic engineering perspective, creating mathematical models upon which to reason and calculate. In its practical facet, this specialization teaches to conceive and animate problem models, testing them in a timely and exhaustive way before proceeding to the calculation and implementation phase, in order to avoid errors of perspective or childish design options.

By resorting to the formal foundations of modelling, reasoning, programming and testing, this offer bears a special mark into the way future professionals are trained to meet high-quality standards in the design of software solutions for real-life problems. This aim is captured by the following «stamp», which software professionals should endeavour to be able to stick to IT products and services:


Teaching staff

ACM Classification

According to IEEE/ACM Curriculum Guidelines for Software Engineering:

  • Software / Software Engineering / Metrics --- 2
  • Software / Software Engineering / Requirements/Specifications --- 6
  • Software / Software Engineering / Software Architectures --- 6
  • Software / Software Engineering / Software/Program Verification --- 6
  • Software / Software Engineering / Testing and Debugging --- 4
  • Theory of Computation / Logics and Meanings of Programs / Specifying and Verifying and Reasoning about Programs --- 6

Required background

  • Experience in programming
  • Familiarity with declarative languages (logical, functional)
  • Predicate logic, lambda calculus and discrete mathematics at first cycle level

Learning Outcomes

  • To create, analyse, refine, classify, animate, test, transform and calculate with abstract models of requirements in software engineering.
  • To transform specifications of complex information systems into efficient implementations on diverse technologies and platforms.
  • To model, analyse, classify and transform component interaction patterns, modular strategies (components, objects, services) and software architectural schemes.
  • To specify, express, and verify the validity of properties (correctness or other properties) of software systems, with the help of automatic and assisted proof tools.
  • To perform software quality control and plan / execute projects in software testing.
  • To document and justify software design decisions based on accurate software modelling and reasoning.
  • To manage software engineering projects in an integrated way from conception to implementation, testing and deployment.





 CSAIL MIT - Software Design Group

 SIG - Software Improvement Group

 Critical Software


home contacts RSS Feed last update: 16-Jun-2021 share facebook
Drupal theme by D7 ver.1.1