@ FII

Formal Methods in Software Engineering

Page contents

• 2024-2025
• Contents
• Useful links and Bibliography
• Course description
  • Software Engineering
  • Distributed Systems
• Schedule
• Email: andrei.arusoaie@uaic.ro

[Top]

Contents

• Basic formal concepts used in software engineering.

• Formalisation of program properties and related notions (invariants, pre/post-conditions).

• Logics for Program Verification.

• Weakest-precondition calculus.

• Strongest-precondition calculus.

• System verification by state exploration.

• Semantics of Programming Languages.

• Symbolic execution and verification based on symbolic execution.

• Type systems.

• Program analysis.

• Tools based on formal methods used in the industry.

[Top]

Useful links and Bibliography

[1] Michael Huth, Mark Ryan. Logic In Computer Science. Modelling and Reasoning about Systems.

[2] Thomas Noll. Static Program Analysis. RWTH Aachen University, 2016/2017 [link].

[3] Flemming Nielson, Hanne R. Nielson, Chris Hankin: Principles of Program Analysis. 2nd edition, Springer, 2005

[4] University of Pennsylvania, CIS 700: Software Analysis and Testing (Fall 2018) [link].

[5] Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, Carolyn Talcott, Maude Manual, 2024 [link].

[6] Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002.

[7] Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, ISBN-13 978-0321143068, 2002.

[8] Glynn Winskel, The formal semantics of programming languages - an introduction. MIT Press 1993, ISBN 978-0-262-23169-5.

[Top]