10.30
12.30 |
ESOP
Semantic Modelling
Session chair: Florence Maraninchi
The Recursive Record Semantics of Objects Revisited
Gerard Boudol (INRIA Sophia Antipolis)
A Formalisation of Java's Exception Mechanism
Bart Jacobs (Nijmegen University)
A Formal Executable Semantics of the JavaCard Platform
G. Barthe, G. Dufay (INRIA, Sophia-Antipolis),
L. Jakubiec (INRIA,
Sophia-Antipolis and Université de Provence),
B. Serpette (INRIA,
Sophia-Antipolis),
S. Melo de Sousa (INRIA, Sophia-Antipolis and
Universidade da Beira Interior)
Modeling an Algebraic Stepper
John Clements, Matthew Flatt, Matthias Felleisen (Rice University) |
FASE
Testing
Session chair: José Fiadeiro
Grammar Testing
Ralf Laemmel (CWI Amsterdam)
Debugging via Run-Time Type Checking
Alexey Loginov, Suan Hsi Yong, Susan Horwitz, Thomas Reps (University
of Wisconsin-Madison)
Library-based Design and Consistency Checking of System-level
Industrial Test Cases
Oliver Niese (METAFrame Technologies, Dortmund),
Bernhard Steffen
(Universität Dortmund),
Tiziana Margaria, Andreas Hagerer (METAFrame Technologies, Dortmund),
Georg
Brune, Hans-Dieter Ide (Siemens, Witten)
Demonstration of an Automated Integrated Testing Environment for CTI
Systems (DEMO)
Oliver Niese, Markus Nagelmann, Andreas Hagerer (METAFrame
Technologies, Dortmund),
Klaus Kolodziejczyk-Strunk (HeraKom, Essen),
Werner Goerigk, Andrei Erochok, Bernhard Hammelmann (Siemens, Witten) |
TACAS
Implementation Techniques
Session chair: Doron Peled
Implementing a Multi-Valued Symbolic Model Checker
Marsha Chechik, Benet Devereux, Steve Easterbrook (University of Toronto)
Is There a Best Symbolic Cycle-Detection Algorithm?
Kathi Fisler (Rice University, Worcester Polytechnic Institute),
Ranan
Fraer (Intel Development Center, Haifa),
Gila Kamhi
(Intel Development Center, Haifa),
Moshe Y. Vardi (Rice University),
Zijiang Yang (Rice University and CCRL, NEC Princeton)
Combining Structural and Enumerative Techniques for the
Validation of Bounded Petri Nets
Rubén Carvajal-Schiaffino, Giorgio Delzanno, Giovanni Chiola
(Università di Genova)
A Sweep-Line Method for State Space Exploration
Søren Christensen (University of Aarhus),
Lars Michael Kristensen
(University of Aarhus and University of South Australia),
Thomas
Mailund (University of Aarhus) |
15.00
17.00 |
ESOP
Static Analysis
Session chair: Hanne Riis Nielson
Typestate Checking of Machine Code
Zhichen Xu, Thomas Reps, Barton P. Miller (University of Wisconsin)
Proof-directed De-compilation of Low-level Code
Shin-ya Katsumata (University of Edinburgh),
Atsushi Ohori (Japan
Advanced Institute of Science and Technology)
Backwards Abstract Interpretation of Probabilistic Programs
David Monniaux (ENS, Paris)
Finding Duplicated Code Using Program Dependences (DEMO)
Raghavan Komondoor, Susan Horwitz
(University of Wisconsin)
|
FASE
Formal Methods
Session chair: Michel Bidoit
Semantics of Architectural Specifications in CASL
Lutz Schroeder, Till Mossakowski (Universität Bremen),
Andrzej
Tarlecki (Warsaw University),
Bartek Klin (BRICS Aarhus),
Piotr
Hoffman (Warsaw University)
Extending Development Graphs with Hiding
Till Mossakowski (Universität Bremen),
Serge Autexier (Universitäat des
Saarlandes),
Dieter Hutter (DFKI, Saarbrücken)
A Logic for the Java Modeling Language JML
Bart Jacobs, Erik Poll (University Nijmegen)
A Hoare-Calculus for Verifying Java Realizations of OCL-Constrained
Design Models
Rolf Hennicker (Ludwig-Maximilans-Universität München),
Bernhard Reus
(University of Sussex at Brighton),
Martin Wirsing
(Ludwig-Maximilans-Universität München) |
TACAS
Semantics and Compositional Verification
Session chair: Perdita Stevens
Assume-Guarantee based Compositional Reasoning for Synchronous
Timing Diagrams
Nina Amla, E. Allen Emerson
(University of Texas at Austin),
Kedar Namjoshi (Bell Laboratories,
Lucent Technologies),
Richard Trefler (AT&T Research)
Simulation Revisited
Li Tan, Rance Cleaveland (State University of New York at Stony Brook)
Compositional Message Sequence Charts
Elsa Gunter (Bell Laboratories),
Anca Muscholl (University of Paris 7),
Doron Peled (Bell Laboratories)
An Automata Based Interpretation of Live Sequence Charts
Jochen Klose (University of Oldenburg),
Hartmut Wittke (OFFIS Oldenburg) |
CMCS |
17.30
19.00 |
ESOP
Logic Programming
Session chair: Radhia Cousot
Compiling Problem Specifications into SAT
Marco Cadoli (Università di Roma),
Andrea Schaerf (Università di Udine)
Semantics and Termination of Simply-Moded Logic Programs
Annalisa Bossi (Università di Venezia),
Sandro Etalle (Universiteit Maastricht and CWI Amsterdam),
Sabina Rossi (Università di Venezia),
Jan-Georg Smaus (CWI Amsterdam)
The Def-inite Approach to Dependency Analysis
Samir Genaim, Michael Codish (Ben-Gurion University) |
FASE
Case Studies
Session chair: Martin Wirsing
A Formal Object-Oriented Analysis for Software Reliability: Design for
Verification
Natasha Sharygina, James C. Browne (University of Texas at Austin),
Robert P. Kurshan (Bell Laboratories)
Specification and Analysis of the AER/NCA Active Network Protocol
Suite in Real-Time Maude
Peter Ölveczky (SRI, Menlo Park),
Mark Keaton (Litton-TASC, Reading),
Jose Meseguer (SRI, Menlo Park),
Carolyn Talcott (Stanford
University),
Steve Zabele (Litton-TASC, Reading) |
TACAS
Logics and Model Checking
Session chair: Wang Yi
Coverage Metrics for Temporal Logic Model Checking
Hana Chockler, Orna Kupferman (Hebrew University),
Moshe Y. Vardi (Rice University)
Parallel Model Checking for the Alternation Free mu-Calculus
Benedikt Bollig, Martin Leucker, Michael Weber (University of Aachen)
Model Checking CTL*[DC]
Paritosh Pandya (Tata Institute of Fundamental Research, Mumbai, India)
|
CMCS |
