You are here: Home Invited Talks
Invited Talks PDF Print E-mail

Dr. Gerard J. Holzmann
Computer Science Department, California Institute of Technology (Caltech)
and NASA Jet Propulsion Laboratory, Laboratory for Reliable Software, Pasadena, USA
FME (Formal Methods Europe) Invited Lecturer to SAFECOMP 2011


Title: Software Safety and Software Complexity

Abstract: It seems to be a general law that all software applications will grow in size and complexity over time. For some important classes of safety-critical systems, the persistent growth rate can even be shown to be exponential. This poses a serious challenge to our ability to perform effective verifications, especially of safety-critical software systems as used in cars, airplanes, and spacecraft. Our methods have to continue to evolve and grow in power as fast as, or ideally faster than, the targets of our investigations do. I will describe how these types of challenges can be tackled.

Short Bio:

Gerard J. Holzmann received his Ph.D. in Technical Sciences from the Delft University of Technology in 1979. From 1980 until 2003 he worked in the Computing Science Research Center of Bell Laboratories, in Murray Hill, New Jersey. In 2003 he joined NASA/JPL in Pasadena, California where he started a new Laboratory for Reliable Software. He is a Senior Research Scientist and a Fellow at JPL, and also serves as Faculty Associate in the Computing Science department of the California Institute of Technology. Dr. Holzmann is best known for the design and implementation of the logic model checker Spin. He holds eight US patents, authored four monographs, and contributed numerous technical articles on software verification, image processing, and telecommunication history. Dr. Holzmann was elected to the U.S. National Academy of Engineering in 2005.


Prof. Paulo Verissimo
Faculty of Sciences, University of Lisbon, Lisbon, Portugal.


Title: Security and Dependability Risks of Critical Information Infrastructures (or why Bang! is different from Crash)

Abstract: This talk is inspired by a contribution to the IEEE Security & Privacy journal, January 2008, answering a question to the “Information Assurance Technology Forecast panel” (*):

Sec&Priv: What’s the nature and magnitude of risk that critical information infrastructure (CII) faces over the next 15 years? By “critical,” I mean the part whose failure would have major effects on a nation, such as economic loss or loss of life.

PJV: Large and ever increasing. Moreover, the objective risk is amplified by the lack of perception of the risk itself existing, by citizens, policy makers, and CII manufacturers and operators. There’s still a belief that the SCADA [Supervisory, Control and Data Acquisition] systems controlling these infrastructures are legacy, closed, obscure, and thus unattackable, or that it suffices to just use a firewall and an intrusion detector. But normal ICT systems protection won’t be enough. To keep a long story short: Ctl-Alt-Del isn’t a remedy for things that have worked continuously for more than 20 years, many security techniques hamper real-time operation, and there’s still a difference between erasing a database and setting a generator on fire. This should be understood immediately or else we should get prepared for the next generation of mass hacking. Maybe all it takes for people to get serious about this is a (Google the remainders of the classical to grasp the basic idea). It might be a good idea for policy makers and CII manufacturers and operators to learn the difference between crash and bang.

(*) FULL PAPER: Information Assurance Technology Forecast 2008, Steven M. Bellovin, Terry V. Benzel, Bob Blakley, Dorothy E. Denning, Whitfield Diffie, Jeremy Epstein, Paulo Veríssimo. IEEE Security & Privacy, vol. 6, no. 1, pp. 10-17, January/February, 2008. [in IEEEexplore]


Short Bio:

Paulo Veríssimo is currently a professor of the Department of Informatics (DI) of the University of Lisboa Faculty of Sciences (, and past Director of LASIGE, a research laboratory of the DI ( He is Fellow of the IEEE and Fellow of the ACM. He is associate editor of the Elsevier Int’l Journal on Critical Infrastructure Protection, and past associate editor of the IEEE Tacs. on Dependable and Secure Computing. He belonged to the European Security & Dependability Advisory Board. He is past Chair of the IEEE Technical Committee on Fault Tolerant Computing and of the Steering Committee of the DSN conference, and belonged to the Executive Board of the CaberNet European Network of Excellence.  He was coordinator of the CORTEX IST/FET project ( Paulo Veríssimo leads the Navigators research group of LASIGE, and is currently interested in: architecture, middleware and protocols for distributed, pervasive and embedded systems, in the facets of real-time adaptability and fault/intrusion tolerance. He is author of more than 150 refereed publications in international scientific conferences and  journals in the area, and co-author of five books (ex.



Prof. Andrea Bondavalli
Dipartimento di Sistemi ed Informatica, University of Florence, Florence, Italy
and ResilTech Srl, Cascina (PI), Italy

Title: Model based resilience assessment of critical information infrastructures

Abstract: The quantitative evaluation of dependability, and resilience of   complex systems, has always been and remains a critical issue. The  complexity of the models used is a very critical problem that needs to be addressed very carefully. Complexity depends on several factors:  the measures to be evaluated, the detail level of the model, the stochastic dependencies among the components, the dynamicity and heterogeneity of the network conditions, the mobility of the actors, the large number of components and scenarios.
The talk provides an overview on some work I performed by in the last years to tackle such problems. The target systems include large-scale critical infrastructures, and mobile distributed systems belonging to different domains, like telecom, automotive and energy.  The talk concludes with some remarks on the open research challenges  in model-based resilience assessment, based on the lesson learned  and on the roadmapping activities carried out within the EC AMBER  Coordination Action.

Short Bio:

Andrea Bondavalli is curently a Professor at the Dipartimento di Sistemi e Informatica, Università degli Studi di Firenze, Firenze, Italy.  Previously he has been a Researcher and a Senior Researcher with the Italian National Research Council, working at the CNUCEInstitute in Pisa, Italy where led the Dependable Computing Group. He has a long experience in participating and leading European funded projects, currently the FP7-SST-2008-RTD-1 234088 ALARP and the ARTEMIS-JU-100022 CHESS. Andrea Bondavalli has authored or co-authored more than 150 papers appeared in International Journals and proceedings of International Conferences. He is a Member of the Editorial Board of the International Journal of Critical Computer-Based Systems, a Member of the Steering Committee of the IEEE SRDS and served as Program Chair and General Chair of many of the most important conference in dependability. Andrea Bondavalli has long dated cooperation and consulting with many companies active on critical application areas and supports the EC as an expert at many levels. He leads the Resilient Computing Lab at UNIFI, and is research interests include critical infrastructures and their architectures, the evaluation and assessment of dependability attributes such as reliability, availability, and performability; and development of design methodologies for real-time dependable systems.