FME program

Sessions take place in auditorium 2 unless otherwise indicated.

Monday July 22nd

Monday's program is also available with abstracts or side by side with other meetings.

08:45-09:55  FLoC opening (joint with LICS, RTA)
Room: auditorium 1
Chair: Moshe Vardi

08:45  Introduction and welcome
08:55  Natarajan Shankar, SRI International, USA
Invited talk: Little engines of proof

10:00-10:30  Session 1: Testing
Chair: Dines Bjørner

10:00  Bruno Legeard, U Franche-Comté, France; Fabien Peureux, U Franche-Comté, France; and Mark Utting, U Waikato, New Zealand
Automated boundary testing from Z and B

10:30-11:00  Refreshments

11:00-12:30  Session 2: Testing
Chair: Bernhard Aichernig

11:00  Gil Ratsaby, Baruch Sterin, and Shmuel Ur; IBM Haifa, Israel
Improvements in coverability analysis
11:30  Juan C. Burguillo-Rial, Manuel J. Fernández-Iglesias, Francisco J. Gonzáles-Castaño, and Martín Llamas-Nistal; U Vigo, Spain
Heuristic-driven test case selection from formal specifications. A case study
12:00  Igor B. Bourdonov, Alexander S. Kossatchev, Victor V. Kuliamin, and Alexander K. Petrenko; ISP/RAS Moscow, Russia
UniTesK test suite architecture

12:30-14:00  Lunch

14:00-15:30  Session 3: Semantics and logic (In memory of John Dawes)
Chair: John Fitzgerald

14:00  David von Oheimb and Tobias Nipkow, Techn. U of Munich, Germany
Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited
14:30  Juan Bicarregui, Rutherford Appleton Laboratory, UK
Do not read this
15:00  Niels Jørgensen, U Roskilde, Denmark
Safeness of make-based incremental recompilation

15:30-16:00  Refreshments

16:00-18:00  Session 4: Model checking support for analysis
Chair: José Oliveira

16:00  Thomas Arts, Ericsson, Sweden; Clara Benac Earle, U Kent-Canterbury, UK; and John Derrick, U Kent-Canterbury, UK
Verifying Erlang code: a resource locker case-study
16:30  Alexandre Mota, Paulo Borba, and Augusto Sampaio; Federal U of Pernambuco, Brazil
Mechanical abstraction of CSPZ processes
17:00  Sharon Barner, Shoham Ben-David, Anna Gringauze, Baruch Sterin, and Yaron Wolfsthal; IBM Haifa, Israel
An algorithmic approach to design exploration
17:30  Michael Huber, Siemens Transportation Systems, Switzerland and Steve King, U York, UK
Towards an integrated model checker for railway signalling data

19:00-21:00  City Hall reception (joint with LICS, RTA)
Room: City Hall

Tuesday July 23rd

Tuesday's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 5: Invited speaker
Chair: Lars-Henrik Eriksson

09:00  Anthony Hall, Praxis Critical Systems, UK
Invited talk: Correctness by construction: Integrating formality into a commercial development process
10:00  Darko Marinov and Sarfraz Khurshid, Massachusetts Inst. of Techn., USA
VAlloy - virtual functions meet a relational language

10:30-11:00  Refreshments

11:00-12:30  Session 6: Smart cards
Chair: Yves Ledru

11:00  Vlad Rusu, IRISA Rennes, France
Verification using test generation techniques
11:30  Néstor Cataño and Marieke Huisman, INRIA Sophia-Antipolis, France
Formal specification and static checking of Gemplus' electronic purse using ESC/Java
12:00  Ludovic Casset, Gemplus Research Laboratory, France
Development of an embedded verifier for Java Card byte code using formal methods

12:30-14:00  Lunch

14:00-15:30  Session 7: Refinement and proof
Chair: Tobias Nipkow

14:00  Michael Backes, Saarland U, Germany; Christian Jacobi, Saarland U, Germany; and Birgit Pfitzmann, IBM Zürich, Switzerland
Deriving cryptographically sound implementations using composition and formally verified bisimulation
14:30  Claus Pahl, Dublin City U, Ireland
Interference analysis for dependable systems using refinement and abstraction
15:00  Neil Henderson, U Newcastle upon Tyne, UK and Stephen Paynter, MBDA Ltd, UK
The formal classification and verification of Simpson's 4-slot asynchronous communication mechanism

15:30-16:00  Refreshments

16:00-17:30  Session 8: Real-time and performance
Chair: Nico Plat

16:00  C. J. Fidge, U Queensland, Australia
Timing analysis of assembler code control-flow paths
16:30  María Victoria Cengarle, Techn. U of Munich, Germany and Alexander Knapp, U Munich, Germany
Towards OCL/RT
17:00  Hubert Garavel, INRIA Rhône-Alpes, France and Holger Hermanns, U Twente, The Netherlands
On combining functional verification and performance evaluation using CADP

19:30-22:30  Conference dinner (joint with LICS, RTA)
Room: Restaurant Luftkastellet

19:30  Banquet
21:30  Martin Davis, U California-Berkeley, USA
Plenary talk: Alan Turing & the advent of the computer

Wednesday July 24th

Wednesday's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 9: Invited speaker
Chair: Peter Lindsay

09:00  David Basin, U Freiburg, Germany
Invited talk: The next 700 synthesis calculi
10:00  Michael Whalen, U Minnesota, USA; Johann Schumann, NASA Ames, USA; and Bernd Fischer, NASA Ames, USA
Synthesizing certified code

10:30-11:00  Refreshments

11:00-12:30  Session 10: Refinement and program verification
Chair: Juan Bicarregui

11:00  Augusto Sampaio, Federal U of Pernambuco, Brazil; Jim Woodcock, U Kent-Canterbury, UK; and Ana Cavalcanti, Federal U of Pernambuco, Brazil
Refinement in Circus
11:30  Ana Cavalcanti, Federal U of Pernambuco, Brazil and David A. Naumann, Stevens Inst. of Techn., USA
Forward simulation for data refinement of classes
12:00  Luke Wildman, U Queensland, Australia
A formal basis for a program compilation proof tools

12:30-14:00  Lunch

14:00-15:30  Session 11: Model checking theory
Chair: Lars-Henrik Eriksson

14:00  Thomas Firley and Ursula Goltz, Techn. U of Braunschweig, Germany
Property dependent abstraction of control structure for software verification
14:30  Natalia Ioustinova, CWI Amsterdam, The Netherlands; Natalia Sidorova, Eindhoven U of Techn., The Netherlands; and Martin Steffen, U Kiel, Germany
Closing open SDL-systems for model checking with DTSpin
15:00  Lars Michael Kristensen, U South Australia, Australia and Thomas Mailund, U Aarhus, Denmark
A generalised sweep-line method for safety properties

15:30-16:00  Refreshments

16:00-17:30  Session 12: Combining methods
Chair: Jim Woodcock

16:00  Helen Treharne, Royal Holloway, U London, UK
Supplementing a UML development process with B
16:30  Jin Song Dong, Jing Sun, and Hai Wang; National U of Singapore
Semantic web for extending and linking formalisms
17:00  Takaaki Umedu, Osaka U, Japan; Yoshiki Terashima, Osaka U, Japan; Keiichi Yasumoto, Nara Inst. of Science and Techn., Japan; Akio Nakata, Osaka U, Japan; Teruo Higashino, Osaka U, Japan; and Kenichi Taniguchi, Osaka U, Japan
A language for describing wireless mobile applications with dynamic establishment of multi-way synchronization channels

17:30-19:00  FME business meeting