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) 1)
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. Among them we recall process algebras, temporal logics, model checking.
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.
The Formal Methods && Tools group is part of the Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - (ISTI), one of the institutes of the Italian National Research Council (Consiglio Nazionale delle Ricerche - CNR)