TACAS at a glance
|
|
|
|
|
||||
|
09:00 |
Invited Lecture Some mistakes I made and what I learned from them Cliff Jones (Harlequin Ltd, UK) |
09:00 |
Invited Lecture Extreme programming: a humanistic discipline of programming Kent Beck (CSLife, CH) |
09:00 |
Invited Lecture Formal verification of pipelined processors Randy Bryant (CMU, USA) |
09:00 |
Invited Lecture Challenges and opportunities visual programming languages bring to programming language research Margaret Burnett (Oregon State U, USA) |
|
10:00 |
Coffee |
10:00 |
Coffee |
10:00 |
Coffee |
10:00 |
Coffee |
|
10: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) |
10: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) |
10: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) |
10: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 |
Lunch |
12:30 |
Lunch |
12:30 |
Lunch |
12:30 |
Lunch |
|
14: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) |
14:30 |
Invited Lecture Practical formal verification: how close are we? Amir Pnueli (Weizmann Institute, IL) |
14:30 |
Invited Lecture Concurrent constraint programming as an extension of functional programming Gert Smolka (U Saarlandes, D) |
||
|
16:30 |
Coffee |
15:30 |
Coffee |
15:30 |
Coffee |
||
|
17:00 |
Panel discussion Paradigms of software science - technical versus human aspects chair: Kai Koskimies (NRC/Hki, FI) |
16: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) |
16: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) |
||
|
18:30 |
Close |
18:00 |
Close |
18:00 |
Close |