![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
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.- 10:00-18:00 in Lobby: Tool demonstrations
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.- 08:30-18:00 in Lobby: Tool demonstrations
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.- 08:30-18:00 in Lobby: Tool demonstrations
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
| FLoC |
|
| MEETINGS |
|
| PROGRAM |
|
| FACILITIES |
|
| COPENHAGEN |
|
| MISCELLANEOUS |
|
