Programme of TACAS at ETAPS 2006
Programme of Monday, March 27
14:00 - 16:00 SESSION 3 (TACAS, Monday)
- Parametrization and Slicing (chair: Holger Hermanns, room: EI 7)
- Automatic Verification of Parameterized Data Structures
- Jyotirmoy Deshmukh, E. Allen Emerson, and Prateek Gupta (The Univ. of Texas at Austin, USA)
- Parameterized Verification of Pi-Calculus Systems
- Ping Yang (SUNY at Stony Brook, USA), Samik Basu, and C.R. Ramakrishnan (Iowa State Univ., USA)
- Easy Parameterized Verification of Biphase Mark and 8N1 Decoders
- Geoffrey M. Brown (Indiana Univ., Bloomington, USA) and Lee Pike (Galois Connections, Inc.)
- Evaluating the Effectiveness of Program Slicing for Model Reduction of Concurrent Object-Oriented Programs.
- Matthew B. Dwyer (Univ. of Nebraska, USA), John Hatcliff, Matthew Hoosier, Venkatesh Ranganath, Robby, and Todd Wallentine (Kansas State Univ., USA)
16:00 - 16:30 Coffee
16:30 - 18:00 SESSION 4 (TACAS, Monday)
- Symbolic Techniques (chair: Jaco van de Pol, room: EI 7)
- New Metrics for Static Variable Ordering in Decision Diagrams
- Radu I. Siminiceanu (National Institute of Aerospace, Hampton, USA) and Gianfranco Ciardo (Univ. of California, Riverside, USA)
- Widening ROBDDs with Prime Implicants
- Neil Kettle, Andy King (Univ. of Kent, Canterbury, UK), and Tadeusz Strzemecki (Fordham Univ., New York, USA)
- Efficient Guided Symbolic Reachability using Reachability Expressions
- Dina Thomas, Supratik Chakraborty (Indian Institute of Technology, Bombay, IND), and Paritosh Pandya (Tata Institute of Fundamental Research, IND)
18:05 - 18:50 EASST MEETING (Monday)
- EASST General Assembly (room: EI 8)
- All EASST members are invited.
19:30 SOCIAL EVENT (Monday)
- Reception in the Vienna City Hall
- The Bürgermeister der Bundeshauptstadt Wien invites all ETAPS participants to a reception in the Rathaus - free admittance
Programme of Tuesday, March 28
10:00 - 12:00 SESSION 2 (TACAS, Tuesday)
- Satisfiability (chair: Gianfranco Ciardo, room: EI 7)
- SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver
- Malay K Ganai (NEC LABS America, Princeton, USA), Murallidhar Talupur (Carnegie Mellon Univ., USA), and Aarti Gupta (NEC LABS America, Princeton, USA)
- SAT-based Software Certification.
- Sagar Chaki (Carnegie Mellon Software Engineering Institute, USA)
- Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants
- Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, and Alwen Tiu (LORIA, INRIA Lorraine / Univ. de Nancy, F)
- Exploration of the Constraint Programming Technique Capabilities in the Software Verification Process
- Hélène Collavizza and Michel Rueher (Univ. de Nice, Sophia-Antipolis, F)
12:00 - 14:00 Lunch
14:00 - 16:00 SESSION 3 (TACAS, Tuesday)
- Abstraction (chair: David Sands, room: EI 7)
- Counterexample-guided Abstraction Refinement for the Analysis of Graph Transformation Systems
- Barbara König and Vitali Kozioura (Univ. of Stuttgart, D)
- Why Waste a Perfectly Good Abstraction?
- Arnie Gurfinkel and Marsha Chechik (Univ. of Toronto, CDN)
- Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking
- Bing Li and Fabio Somenzi (Univ. of Colorado at Boulder, USA)
- Approximating Predicate Images for Bit-Vector Logic
- Daniel Kröning (ETH Zürich, CH) and Natasha Shrygina (Univ. of Lugano, CH)
16:00 - 16:30 Coffee
16:30 - 18:00 SESSION 4 (TACAS, Tuesday)
- Model Checking Algorithms (chair: Kenneth McMillan, room: EI 7)
- Finitary Winning in ω-Regular Games
- Krishnendu Chatterjee (Univ. of California, Berkeley, USA) and Thomas A. Henzinger (Univ. of California, Berkeley, USA, and EPFL, CH)
- Efficient Model Checking for LTL with Partial Order Snapshots
- Peter Niebert (Laboratoire d'Informatique Fondamentale de Marseille, F) and Doron Peled (Univ. of Warwick, UK)
- A Local Shape Analysis based on Separation Logic
- Dino Distefano, Peter W. O'Hearn (Queen Mary, Univ. of London, UK), and Hongseok Yang (Seoul National Univ., ROK)
19:30 SOCIAL EVENT (Tuesday)
- Main Conference Banquet in the Orangery of Schönbrunn Palace
- Tickets needed - see registration
Programme of Wednesday, March 29
08:30 - 09:30 SESSION 1 (Wednesday)
- Unifying Invited Talk (chair: Perdita Stevens, room: EI 7)
- Software Engineering: Emerging Goals and Lasting Problems
- Carlo Ghezzi (Politecnico di Milano, I)
09:30 - 10:00 Coffee
10:00 - 12:00 SESSION 2 (TACAS, Wednesday)
- Program Verification (chair: Lenore Zuck, room: EI 7)
- Compositional Model Extraction for Higher-Order Concurrent Programs
- Dan Ghica (Univ. of Birmingham, UK) and Andrzej Murawski (Oxford Univ. Computing Laboratory, UK)
- A Region Graph Based Approach to Termination Proofs
- Stefan Leue and Wei Wei (Univ. of Konstanz, D)
- Verifying Concurrent Message-Passing C Programs with Recursive Calls
- Sagar Chaki, Edmund Clarke (Carnegie Mellon Univ., USA), Nicholas Kidd, Thomas Reps (Univ. of Wisconsin, USA), and Tayssir Touili (LIAFA, CNRS and Univ. Paris 7, F)
- Automata-based Verification of Programs with Tree Updates
- Peter Habermehl (LIAFA / Univ. Paris 7, F), Radu Iosif (VERIMAG/CNRS, F), and Tomas Vojnar (Brno Univ. of Technology, CZ)
12:00 - 14:00 Lunch
14:00 - 15:00 SESSION 3A (Wednesday)
- Unifying Invited Talk (chair: Jens Knoop, room: EI 7)
- The Weird World of Bi-Directional Programming
- Benjamin Pierce (Univ. of Pennsylvania, USA)
15:00 - 15:15 Break
15:15 - 16:15 SESSION 3B (TACAS, Wednesday)
- Runtime Diagnostics (chair: Rance Cleaveland, room: EI 7)
- An Experimental Comparison of the Effectiveness of Control flow Based Testing Approaches on Seeded Faults
- Atul Gupta and Pankaj Jalote (Indian Institute of Technolgoy, Kanpur, IND)
- Exploiting Traces in Program Analysis
- Alex Groce and Rajeev Joshi (California Institute of Technology, Pasadena, USA)
16:15 - 16:45 Coffee
16:45 - 18:15 SESSION 4 (TACAS, Wednesday)
- Quantitative Techniques (chair: Kim G. Larsen, room: EI 7)
- Model-Checking Markov Chains in the presence of Uncertainties
- Koushik Sen, Mahesh Viswanathan, and Gul Agha (Univ. of Illinois at Urbana-Champaign, USA)
- Safety Metric Temporal Logic is Fully Decidable
- Joel Ouaknine and James Worrell (Oxford Univ. Computing Laboratory, UK)
- Simulation-Based Graph Similarity
- Oleg Sokolsky, Sampath Kannan, and Insup Lee (Unversity of Pennsylvania, USA)
19:30 SOCIAL EVENT (Wednesday)
Heuriger
- This is the Viennese term for the wine of the most recent grape harvest, and it is also the name of the places where the wine is served. Enjoy Viennese wine and local food at the Heurigen Schübel-Auer, Kahlenberger Straße 22, Wien-Nußdorf. Free admittance to ETAPS participants.
Programme of Thursday, March 30
08:30 - 09:30 SESSION 1 (TACAS, Thursday)
- Invited Talk (chair: Jens Palsberg, room: EI 7)
- Distributed Model-Checking Algorithms for WPDS with Applications to Trust-Management Systems
- Somesh Jha (Univ. of Wisconsin, Madison, USA)
09:30 - 10:00 Coffee
10:00 - 12:00 SESSION 2 (TACAS, Thursday)
- TACAS/SPIN Tool Demonstrations (chair: Thierry Jeron, room: EI 7)
- PRISM: A Tool for Automatic Verification of Probabilistic Systems
- Andrew Hinton, Marta Kwiatkowska, Gethin Norman, and David Parker (Univ. of Birmingham, UK)
- DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation
- Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, and Gilles Stragier (INRIA Rhône-Alpes / VASY, F)
- MCMAS: a Model Checker for Multi-Agent Systems
- Franco Raimondi and Alessio Lomuscio (Univ. College London, UK)
- A Counterexample-Guided Refinement Tool for Open Procedural Programs
- Aleksandar Dimovski (Univ. of Warwick, UK), Dan R. Ghica (Univ. of Birmingham, UK), and Ranko Lazić (Univ. of Warwick, UK)
15:15 - 16:15 SESSION 3B (TACAS, Thursday)
- TACAS/SPIN Tool Demonstrations (chair: Susanne Graf, room: EI 7)
- jMosel: A Stand-Alone Tool and jABC Plugin for M2L(Str)
- Christian Topnik, Eva Wilhelm (Univ. Dortmund, D), Tiziana Margaria (Univ. Göttingen, D), and Bernhard Steffen (Univ. Dortmund, D)
- MSCan -- A Tool for Analyzing MSC Specifications
- Benedikt Bollig (LSV, CNRS Cachan, F), Carsten Kern, Markus Schlütter, and Volker Stolz (RWTH Aachen, D)
16:15 - 16:45 Coffee
16:45 - 18:15 SESSION 4 (TACAS, Thursday)
- Refinement (chair: Michael Huth, room: EI 7)
- A Practical and Complete Approach to Predicate Refinement
- Ranjit Jhala (Univ. of California, San Diego, USA) and Kenneth L. McMillan (Cadence Berkeley Lab, USA)
- Counterexample Driven Refinement for Abstract Interpretation
- Bhargav S. Gulavanii (Indian Institute of Technology, Bombay, IND) and Sriram K. Rajamani (Microsoft Research Lab, IND)
- Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems
- Javier Esparza, Stefan Kiefer, and Stefan Schwoon (Univ. of Stuttgart, D)
19:30 SOCIAL EVENT (Thursday)
- Reception
- Intel invites all ETAPS participants to a reception in the Prechtlsaal of the TU Main Building, Karlsplatz 13, 1040 Wien - free admittance
Further ETAPS 2006 Programme Information:
- Programme Overview
- Main Conferences:
Complete Programme,
CC,
ESOP,
FASE,
FOSSACS
- Workshops:
ACCAT,
AVIS,
CMCS,
COCV,
DCC,
EAAI,
FESCA,
FRCSS,
GT-VMT,
LDTA,
MBT,
QAPL,
SC,
SLAP,
SPIN,
TERMGRAPH,
WITS,
WRLA
- Tutorials:
Phoenix,
QuantComp
ETAPS 2006 |
Top |
HTML 4.01 |
Last Update: 2006-03-23