FM 2008

Invited Speakers

The following distinguished speakers have accepted to give an invited lecture at FM'08:

Professor ArvindMassachusetts Institute of Technology
Project Officer Paolo BrescianiEuropean Comission, Brussels
Professor Dawson EnglerStanford University
Professor Shmuel KatzThe Technion
Professor Jay MisraThe University of Texas at Austin


Prof. Arvind "Getting Formal Verification into Design Flow"

Abstract: The ultimate goal of formal methods is to provide assurances about the quality, performance, security, etc. of systems. While formal tools have advanced greatly over the past two decades, widespread proliferation has not yet occurred, and the full impact of formal methods is still to be realized. This paper presents some ideas on how to catalyze the growth of formal techniques in day-to-day engineering practice. We draw on our experience as hardware engineers that want to use, and have tried to use, formal methods in our own designs. The points we make have probably been made before. However we illustrate each one with concrete designs. Our examples support three major themes: (1) correctness depends highly on the application and even a collection of formal methods cannot handle the whole problem; (2) high-level design languages can facilitate the interaction between design and formal methods; and (3) formal method tools should be presented as integrated debugging aids as opposed to one requiring mastering a foreign language or esoteric concepts.

Presentation (PDF)

Project Officer Paolo Bresciani "The ICT theme in the FP7: towards the Work Program 2009-2010"

After one year and a half since its launch in December 2006, the Seventh Research Framework Programme entered its fully operational phase: in the thematic area of ICT, three calls have now been closed, and the first projects from the first call are now fully running. In this talk I will briefly resume the transition form FP6 to FP7 and introduce the role of the ICT theme in the Seventh Research Framework Programme, focusing in particular on the area of Software and Services Engineering. We are now approaching the end of the Work-Programme 2007-2008 period. Details on the first activities and future steps towards the definition of the next WP 2009-2010 will be provided as well.

Prof. Dawson Engler "Lessons in the weird and unexpected: some experiences from checking large real systems"

Abstract: This talk will draw on our efforts in using static analysis, model checking, and symbolic execution to find bugs in real code, both in academic and commercial settings. The unifying religion driving all these efforts has been: results matter more than anything. That which works is good, that which does not is not. While this worldview is simple, reality is not. I will discuss some what we learned in struggling with this mismatch.

Prof. Shmuel Katz "Aspects and Formal Methods"

Abstract: Aspects are now commonly used to add functionality that otherwise would cut across the structure of object systems. In this survey, both directions in the connection between aspects and formal methods are examined. On the one hand, the use of aspects to facilitate (general) software verification, and especially model checking, is demonstrated. On the other hand, the new challenges to formal specification and verification posed by aspects are defined, and several existing solutions are described.

Prof. Jay Misra "Simulation, Orchestration and Logical clocks"

Abstract: A language in which discrete event simulations can be coded needs to support the features (1) to describe behavior of a single physical process, (2) to describe concurrent activities of multiple physical processes, including communication, synchronization and interruption, (3) to account for passage of time, and (4) to record system state at appropriate points and create statistical summaries. Orc, a recent language for orchestration of distributed services, combines these features so that complex simulations can be expressed very succinctly. This talk describes the relevant features of Orc for simulation and illustrates them using a number of realistic examples. Additionally, we show that certain combinatorial problems, such as shortest paths in graphs and many problems in computational geometry, can be cast as simulation problems, and solved very simply in Orc.