TACAS
Tools and Algorithms for the Construction and Analysis of Systems
Programme Commitee
B. Steffen (Germany, chair), E. Brinksma (Netherlands), R. Cleaveland (USA), F. Giunchiglia (Italy), S. Graf (France), T. Henzinger (USA), D. Jackson (USA), K. Jensen (Denmark), K. Larsen (Denmark), T. Margaria (Germany), J. Palsberg (Denmark), D. Peled (USA), S. Smolka (USA), F. Vaandrager (Netherlands)
PROGRAMME
09:00 10:00
|
Invited Lecture Some mistakes I made and what I learned from them Cliff Jones (Harlequin Ltd, UK) |
10:00 10:30
|
Coffee |
10:30 12:30
| Fully local and efficient evaluation of alternating fixed points,
X.Liu, CR.Ramakrishnan and SA.Smolka (State U New York at Stony Brook,
USA)
Modular model checking of software, K.Laster and O.Grumberg (Technion, IL) Verification based on local states, M.Huhn, P.Niebert (U Hildesheim, D) and F.Wallner (U Munich, D) Exploiting symmetry in linear time temporal logic model checking: one step beyond, K.Ajami (U Pierre et Marie Curie, F), S.Haddad (U Pierre et Marie Curie, F) and J-M.Ilie (U Paris Dauphine, F) |
12:30 14:30
|
Lunch |
14:30 16:30
| Open/Caesar: an open software architecture for verification, simulation,
and testing, H.Garavel (INRIA, F)
Practical model checking using games, P.Stevens and C.Stirling (U Edinburgh, UK) Combining finite automata, parallel programs and SDL using Petri nets, B.Grahlmann (U Hildesheim, D) MESA: support for scenario-based design of concurrent systems, H.Ben-Abdallah (U Sfax, TN) and S.Leue (U Waterloo, CA) |
16:30 17:00
|
Coffee |
17:00 18:30
|
Panel discussion Paradigms of software science - technical versus human aspects chair: Kai Koskimies (NRC/Hki, FI) |
09:00 10:00
|
Invited Lecture Extreme programming: a humanistic discipline of programming Kent Beck (CSLife, CH) |
10:00 10:30
|
Coffee |
10:30 12:30
| Efficient modeling of memory arrays in symbolic ternary simulation,
MN.Velev and R.Bryant (CMU, USA)
Translation validation, A.Pnueli, M.Siegel (Weizmann Institute, IL) and E.Singerman (SRI, USA) A verified model checker for the modal µ-calculus in Coq, C.Sprenger (Swiss Federal Institute of Technology, CH) Detecting races in relay ladder logic programs, A.Aiken, M.Fähndrich and Z.Su (U California at Berkeley, USA) |
12:30 14:30
|
Lunch |
14:30 15:30
|
Invited Lecture Practical formal verification: how close are we? Amir Pnueli (Weizmann Institute, IL) |
15:30 16:00
|
Coffee |
16:00 18:00
| Verification of large state/event systems using compositionality
and dependency analysis, J.Lind-Nielsen, HR.Andersen (TU Denmark, DK),
G.Behrmann (Aalborg U, DK), H.Hulgaard (TU Denmark, DK) , K.Kristoffersen
and KG.Larsen (Aalborg U, DK)
Tamagotchis need not die - verification of STATEMATE designs, U.Brockmeyer and G.Wittich (OFFIS, Oldenburg, D) Modeling and verification of sC++ applications, T.Cattel (École Polytechnique Fédérale, CH) Factotum: automatic and systematic sharing support for systems analyzers, DJ.Sherman and N.Magnier (U Bordeaux, F) |
09:00 10:00
|
Invited Lecture Formal verification of pipelined processors Randy Bryant (CMU, USA) |
10:00 10:30
|
Coffee |
10:30 12:30
| Model checking via reachability testing for timed automata,
L.Aceto (Aalborg U, DK), A.Burgueno (ONERA-CERT, F) and KG.Larsen (Aalborg
U, DK)
Formal design and analysis of a gear controller: an industrial case study using UPPAAL, M.Lindahl (Mecel AB, S), P.Pettersson and W.Yi (Uppsala U, S) Verifying networks of timed processes, P. Aziz Abdulla and B.Jonsson (Uppsala U, S) Model checking of real-time reachability properties using abstractions, C.Daws and S.Tripakis (VERIMAG, F) |
12:30 14:30
|
Lunch |
14:30 15:30
|
Invited Lecture Concurrent constraint programming as an extension of functional programming Gert Smolka (U Saarlandes, D) |
15:30 16:00
|
Coffee |
16:00 18:00
| Symbolic exploration of transition hierarchies, R.Alur (U Pennsylvania,
USA), TA.Henzinger and SK.Rajamani (U California at Berkeley, USA)
Static partial order reduction, R.Kurshan, V.Levin, M.Minea, D.Peled and H.Yenigün (Bell Labs, USA) Set-based analysis of reactive infinite-state systems, W.Charatonik and A.Podelski (Max-Planck-Institut, D) Deciding fixed and non-fixed size bit-vectors, NS.Bjørner and M.Pichora (Stanford U, USA) |
09:00 10:00
|
Invited Lecture Challenges and opportunities visual programming languages bring to programming language research Margaret Burnett (Oregon State U, USA) |
10:00 10:30
|
Coffee |
10:30 12:30
| Experience with literate programming in the modelling and validation
of systems, TC.Ruys and E.Brinksma (U Twente, NL)
A proof of Burns n-process mutual exclusion algorithm using abstraction, HE.Jensen (Aalborg U, DK) and N.Lynch (MIT, USA) Automated verification of Szymanski's algorithm, EP.Gribomont and G.Zenner (U Liège, B) Formal verification of SDL systems at the Siemens mobile phone department, F.Regensburger and A.Barnard (Siemens AG, D) |
12:30 14:30
|
Lunch |