Programme of TACAS at ETAPS 2007
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
- Cocktail/Buffet
- 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:
- Programme Overview, Social Programme
- Main Conferences:
Complete Programme,
CC,
ESOP,
FASE,
FOSSACS
- Workshops:
ACCAT,
Bytecode,
COCV,
FESCA,
FinCo,
GT-VMT,
HAV,
HFL,
LDTA,
MBT,
MOMPES,
OpenCert,
QAPL,
SC,
SLA++P,
TERMGRAPH,
WITS
- Tutorials:
Stratego/XT,
SoftwGen,
Mobius
ETAPS 2007 |
Top |
HTML 4.01 |
Last Update: 2007-03-21