Formal Methods and Tools Laboratory (FMT)

home | people | topics | projects | publications | software | news



Head: Stefania Gnesi

Formal Methods play a major role in computer engineering and in the broader context of system engineering, where also the interaction of machines with humans is taken into consideration. In fact:

"All engineering disciplines make progress by employing mathematically based notations and methods. Research on `formal methods' follows this model and attempts to identify and develop mathematical approaches that can contribute to the task of creating computer systems (both their hardware and software components)*

(*) Cliff Jones, "Thinking Tools for the Future of Computing Science" in R. Wilhelm, editor. Informatics 10 Years Back 10 Years Ahead, Lecture Notes in Computer Science volume 2000. Springer-Verlag, 2000.

The very origins of FM go back to Mathematical Logic, or, more precisely, to that branch of Mathematical Logic which gave rise to Logics in Computer Science (LICS) and Theoretical Computer Science (TCS). Several fields of LICS and TCS have contributed to the development of the foundations of FM, like language and automata theory, Petri Nets, programming/specification language syntax and semantics, and program verification.

More recently, solid contributions to the specification and analysis of systems in particular concurrent/distributed systems have been provided.

The Formal Methods && Tools Group is active in the fields of development and application of formal notations, methods and software support tools for the specification, design and verification of complex computer systems. These efforts are based mostly on the foundational concepts and techniques of process algebras, temporal logics, model checking. Members of the FM&&T group are also active in the areas of computer ethics and information technology and society, and of formal approaches to Requirement Engineering.

comments to Stefania Gnesi