Programme of TACAS at ETAPS 2007

Tools and Algorithms for the Construction and Analysis of Systems

Programme of Monday, March 26

11:00 - 12:30 SESSION 2 (Monday)

Software Verification (Chair: Natasha Sharygina, room: Enabler-Wipro)
Shape Analysis by Graph Decomposition
Roman Manevich (Tel Aviv University), Joshua Berdine, Byron Cook (Microsoft Reasearch Cambridge), Ganesan Ramalingam (Microsoft Research India), and Mooly Sagiv (Tel Aviv University)
A reachability predicate for analyzing low-level software
Shaunak Chatterjee (Indian Institute of Technology at Kharagpur), Shuvendu K. Lahiri, Shaz Qadeer (Microsoft Research), and Zvonimir Rakamaric (University of British Columbia)
Generating Representation Invariants of Structurally Complex Data
Muhammad Zubair Malik, Aman Pervaiz, and Sarfraz Khurshid (University of Texas at Austin)

12:30 - 14:30 Lunch

14:30 - 16:30 SESSION 3 (Monday)

Probabilistic Model Checking and Markov Chains (Chair: Holger Hermanns, room: Enabler-Wipro)
Multi-Objective Model Checking of Markov Decision Processes
Kousha Etessami (University of Edinburgh), Marta Kwiatkowska (Birmingham University), Moshe Y. Vardi (Rice University), and Mihalis Yannakakis (Columbia University)
PReMo: an analyzer for Probabilistic Recursive Models
Dominik Wojtczak and Kousha Etessami (University of Edinburgh)
Counterexamples in Probabilistic Model Checking
Tingting Han and Joost-Pieter Katoen (RWTH Aachen and University of Twente)
Bisimulation minimisation mostly speeds up probabilistic model checking
Joost-Pieter Katoen (RWTH Aachen and University of Twente), Tim Kemna (University of Twente), Ivan Zapreev (RWTH Aachen and University of Twente), and David N. Jansen (University of Twente)

16:30 - 17:00 Coffee

17:00 - 18:30 SESSION 4 (Monday)

Static Analysis (Chair: Tiziana Margaria, room: Enabler-Wipro)
Causal Concurrent Dataflow Analysis for Concurrent Programs
Azadeh Farzan and P. Madhusudan (University of Illinois at Urbana-Champaign)
Type-dependency Analysis and Program Transformation for Symbolic Execution
Saswat Anand, Alessandro Orso, and Mary Jean Harrold (Georgia Institute of Technology)
JPF--SE: A Symbolic Execution Extension to Java PathFinder
Saswat Anand (Georgia Institute of Technology), Corina S. Pasareanu, and Willem Visser (NASA Ames Research Center)

19:00 SOCIAL EVENT (Monday)

Welcome Reception (free admittance)
Largo do Paço (University Rectorate Building)
The Etaps Organization invites all ETAPS participants to the welcome reception - free admittance

Programme of Tuesday, March 27

10:30 - 12:30 SESSION 2 (Tuesday)

Markov Chains and Real-Time Systems (Chair: Joost-Pieter Katoen, room: Enabler-Wipro)
A Symbolic Algorithm for Optimal Markov Chain Lumping
Salem Derisavi (Carleton University at Ottawa)
Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
Lijun Zhang, Holger Hermanns (Saarland University), Friedrich Eisenbrand (University of Paderborn), and David N. Jansen(University of Twente)
Model Checking Probabilistic Timed Automata with One or Two Clocks
Marcin Jurdzinski (University of Warwick), Francois Laroussinie (ENS Cachan), and Jeremy Sproston (Universita di Torino)
Adaptor synthesis for real-time components
Massimo Tivoli (University of L'Aquila), Pascal Fradet, Alain Girault, Gregor Goessler (INRIA Rhone-Alpes)

12:30 - 14:30 Lunch

14:30 - 16:30 SESSION 3 (Tuesday)

(I) Timed Automata and Duration Calculus (Chair: Joel Ouaknine, room: Cisco)
Deciding an Interval Logic with Accumulated Durations
Martin Fraenzle (Universitat Oldenburg) and Michael R. Hansen (Technical University of Denmark)
From Time Petri Nets to Timed Automata: an Untimed Approach
Davide D'Aprile, Susanna Donatelli (Universita di Torino), Arnaud Sangnier (LSV-ENS Cachan), and Jeremy Sproston (Universita di Torino)
Complexity in Simplicity: Flexible Agent-based State Space Exploration
Jacob Illum Rasmussen, Gerd Behrmann, and Kim G. Larsen (Aalborg University)
On Sampling Abstraction of Continuous Time Logic with Durations
Paritosh K. Pandya (Tata Institute of Fundamental Research), Shankara Narayanan Krishna, and Kuntal Loya (Indian Institute of Technology at Bombay)
(II) Assume-Guarantee Reasoning (Chair: Moshe Vardi, room: Multicert)
Assume Guarantee Synthesis
Krishnendu Chatterjee (University of California, Berkeley) and Thomas A. Henzinger (EPFL)
Optimized L* for Assume-Guarantee Reasoning
Sagar Chaki (Software Engineering Institute) and Ofer Strichman (The Technion, Haifa)
Refining Interface Alphabets for Compositional Verification
Mihaela Gheorghiu (University of Toronto), Dimitra Giannakopoulou, and Corina S. Pasareanu NASA Ames Research Center)
MAVEN: Modular Aspect Verification
Max Goldman and Shmuel Katz (The Technion, Haifa)

16:30 - 17:00 Coffee

17:00 - 18:30 SESSION 4 (Tuesday)

Biological Systems (Chair: Radha Jagadeesan, room: Enabler-Wipro)
Model Checking Liveness Properties of Genetic Regulatory Networks
Gregory Batt and Calin Belta (Boston University), and Ron Weiss (Princeton University)
Checking Pedigree Consistency with SAT
Panagiotis Manolios, Marc Galceran Oms, and Sergi Oliva Valls (Georgia Institute of Technology, Atlanta)
Don't Care Modeling: A logical framework for developing predictive system models
Hillel Kugler (New York University), Amir Pnueli (New York University and the Weizmann Institute of Science), Michael Stern (Yale University), and E. Jane Albert Hubbard (New York University)

19:00 SOCIAL EVENT (Tuesday)

10th Anniversary Celebration (free admittance)
Theatro Circo
Tales of ETAPS past (room: Enabler-Wipro)
Anniversary Cake + Port Wine + Fado Concert

Programme of Wednesday, March 28

09:00 - 10:10 SESSION 1 (Wednesday)

Unifying Invited Talk (Chair: Perdita Stevens, room: Enabler-Wipro)
There and Back Again: Lessons Learned on the Way to the Market
Rance Cleaveland (University of Maryland/Fraunhofer USA Center for Experimental Software Engineering and Reactive Systems Inc., USA)

10:10 - 10:30 Coffee

10:30 - 12:30 SESSION 2 (Wednesday)

Abstraction Refinement (Chair: Shmuel Katz, room: Enabler-Wipro)
Deciding Bit-Vector Arithmetic with Abstraction
Randal E. Bryant (Carnegie Mellon University), Daniel Kroening (ETH Zuerich), Joel Ouaknine (Oxford University), Sanjit A. Seshia (University of California, Berkeley), Ofer Strichman (The Technion, Haifa), and Bryan Brady (University of California, Berkeley)
Abstraction Refinement of Linear Programs with Arrays
Alessandro Armando (Universita di Genova), Massimo Benerecetti (Universita di Napoli), and Jacopo Mantovani (Universita di Genova)
Property-Driven Partitioning for Abstraction Refinement
Roberto Sebastiani (Universita di Trento), Stefano Tonetta (University of Lugano), and Moshe Y. Vardi (Rice University)
Combining Abstraction Refinement and SAT-based Model Checking
Nina Amla and Kenneth McMillan (Cadence Design Systems)

12:30 - 14:30 Lunch

14:30 - 15:40 SESSION 3A (Wednesday)

Invited Talk (Chair: Rance Cleaveland, room: Enabler-Wipro)
Verifying object-oriented software: lessons and challenges
K. Rustan M. Leino (Microsoft Research, Redmond, USA)

15:40 - 15:50 Break

15:50 - 16:50 SESSION 3B (Wednesday)

Message Sequence Charts (Chair: Nina Amla, room: Enabler-Wipro)
Detecting Races in Ensembles of Message Sequence Charts
Edith Elkind (University of Liverpool), Blaise Genest (CNRS/IRISA), and Doron Peled (Bar Ilan University)
Replaying Play in and Play out: Synthesis of Design Models from Scenarios by Learning
Benedikt Bollig (LSV CNRS Cachan), Joost-Pieter Katoen, Carsten Kern (RWTH Aachen University), and Martin Leucker (TU Munich)

16:50 - 17:15 Coffee

17:15 - 18:45 SESSION 4 (Wednesday)

Automata-Based Model Checking (Chair: Daniel Kroening, room: Enabler-Wipro)
Improved algorithms for the automata based approach to model-checking
Laurent Doyen (EPFL) and Jean-Francois Raskin (Universitat Libre de Bruxelles)
GOAL: A Graphical Tool for Manipulating Buechi Automata and Temporal Formulae
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Kang-Nien Wu, and Wen-Chin Chan (National Taiwan University)
Faster Algorithms for Finitary Games
Florian Horn (LIAFA, Universite Paris 7)

19:00 SOCIAL EVENT (Wednesday)

Conference Banquet (tickets needed)
Paço dos Duques, Guimarães
Shuttle departure from Theatro Circo

Programme of Thursday, March 29

10:30 - 12:30 SESSION 2 (Thursday)

Specification Languages (Chair: Marsha Chechik, room: Enabler-Wipro)
Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs
David Harel and Itai Segall (The Weizmann Institute of Science)
MoToR: The MoDeST Tool Environment
Henrik Bohnenkamp (RWTH Aachen University), Holger Hermanns (Saarland University), and Joost-Pieter Katoen (RWTH Aachen University and University of Twente)
Syntactic Optimizations for PSL Verification
Alessandro Cimatti, Marco Roveri (ITC-irst Trento), and Stefano Tonetta (University of Lugano)
The Heterogeneous Tool Set
Till Mossakowski, Christian Maeder (DFKI Lab and University of Bremen), and Klaus Luettich (SFB/TR 8 and University of Bremen)

12:30 - 14:30 Lunch

14:30 - 15:30 SESSION 3A (Thursday)

Unifying Invited Talk (Chair: João Saraiva, room: Enabler-Wipro)
Contract-Driven Development
Bertrand Meyer (ETH Zürich, Switzerland)

15:40 - 15:50 Break

15:50 - 16:50 SESSION 3B (Thursday)

Security (Chair: Michael Huth, room: Enabler-Wipro)
Searching for Shapes in Cryptographic Protocols
Shaddin F. Doghmi, Joshua D. Guttman, and F. Javier Thayer (The MITRE Corporation)
Automatic Analysis of the Security of XOR-based Key Management Schemes
Veronique Cortier (Loria and CNRS and INRIA), Gavin Keighren, and Graham Steel (University of Edinburgh)

16:50 - 17:15 Coffee

17:15 - 18:45 SESSION 4 (Thursday)

Software and Hardware Verification (Chair: Orna Grumberg, room: Enabler-Wipro)
State of the Union: Type Inference via Craig Interpolation
Ranjit Jhala (UC San Diego), Rupak Majumdar, and Ru-Gang Xu (UC Los Angeles)
Hoare Logic for Realistically Modelled Machine Code
Magnus O. Myreen and Michael J. C. Gordon (University of Cambridge)
VCEGAR: Verilog CounterExample Guided Abstraction Refinement
Himanshu Jain (Carnegie Mellon University), Daniel Kroening (ETH Zuerich), Natasha Sharygina (Carnegie Mellon University and University of Lugano), and Edmund Clarke (Carnegie Mellon University)

Programme of Friday, March 30

10:30 - 12:30 SESSION 2 (Friday)

Decision Procedures and Theorem Provers (Chair: Parosh Abdulla, room: Multicert)
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications
Marcelo F. Frias, Carlos G. Lopez Pombo, and Mariano M. Moscato (Universidad de Buenos Aires and CONICET)
Combined Satisfiability Modulo Parametric Theories
Sava Krstic, Amit Goel, Jim Grundy (Intel Corporation), and Cesare Tinelli (The University of Iowa)
A Groebner Basis Approach to CNF-formulae Preprocessing
Christopher Condrat and Priyank Kalla (University of Utah)
Kodkod: A Relational Model Finder
Emina Torlak and Daniel Jackson (Massachusetts Institute of Technology)

12:30 - 14:30 Lunch

14:30 - 16:30 SESSION 3 (Friday)

Model Checking (Chair: Orna Grumberg, room: Multicert)
Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams
Jinqing Yu, Gianfranco Ciardo (University of California, Riverside), and Gerald Luettgen (University of York)
Model Checking of Tree Logics with Path Equivalences
Rajeev Alur, Pavol Cerny, and Swarat Chaudhuri (University of Pennsylvania)
Uppaal/DMC - Abstraction-based Heuristics for Directed Model Checking
Sebastian Kupferschmid (University of Freiburg), Klaus Drager (Universitat des Saarlandes), Jorg Hoffmann (Digital Enterprise Research Institute, Innsbruck), Berd Finkbeiner (Universitat des Saarlandes), Henning Dierks (OFFIS, Oldenburg), Andreas Podelski (University of Freiburg), Gerd Behrmann (Aalborg University)
mCRL Distributed State Space Generation in Practice
Stefan Blom (Universitat Innsbruck), Jens R. Calame, Bert Lisser (CWI, Amsterdam), Simona Orzan (TU/e, Eindhoven), Jun Pang (Carl von Ossietzky Universitat, Oldenburg), Jaco van de Pol (CWI, Amsterdam and TU/e, Eindhoven), Mohammad Torabi Dashti, and Anton J. Wijs (CWI, Amsterdam)

16:30 - 17:00 Coffee

17:00 - 18:30 SESSION 4 (Friday)

Infinite-State Systems (Chair: Michael Huth, room: Multicert)
A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
Ahmed Bouajjani, Yan Jurski, and Mihaela Sighireanu (LIAFA, University of Paris 7)
Unfolding Concurrent Well-Structured Transition Systems
Frederic Herbreteau, Gregoire Sutre, and The Quang Tran (LaBRI, Bordeaux)
Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems)
Parosh Aziz Abdulla (Uppsala University), Giorgio Delzanno (Universita di Genova), Noomene Ben Henda, and Ahmed Rezine (Uppsala University)

Further ETAPS 2007 Programme Information:

ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-21