Programme of TACAS at ETAPS 2006

Tools and Algorithms for the Construction and Analysis of Systems

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:

ETAPS 2006 | Top | HTML 4.01 | Last Update: 2006-03-23