Programme of TACAS at ETAPS 2008

Tools and Algorithms for the Construction and Analysis of Systems

Programme of Monday, March 31

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

PARAMETERIZED SYSTEMS (room: Star)
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
Azadeh Farzan, Yu-Fang Chen, Edmund Clarke, Yih-Kuen Tsay and Bow-Yaw Wang
Graph Grammar Modeling and Verification of Ad Hoc Routing Protocols
Mayank Saksena, Oskar Wibling and Bengt Jonsson
Proving Ptolemy Right: The Environment Abstraction Principle for Model Checking Concurrent Systems
Edmund Clarke, Muralidhar Talupur and Helmut Veith

12:30 - 14:30 Lunch

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

MODEL CHECKING I (room: Star)
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking
Jiri Barnat, Lubos Brim, Pavel Simecek and Michael Weber
Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
Martin De Wulf, Laurent Doyen, Nicolas Maquet and Jean-Francois Raskin
On-the-Fly Techniques for Games-Based Software Model Checking
Adam Bakewell and Dan Ghica
Computing Simulations over Tree Automata
Parosh Abdulla, Ahmed Bouajjani, Lukas Holik, Lisa Kaati and Tomas Vojnar

16:30 - 17:00 Coffee

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

APPLICATIONS (room: Star)
Formal Pervasive Verification of a Paging Mechanism
Eyad Alkassar, Norbert Schirmer and Artem Starostin
Analyzing Stripped Device-Driver Executables
Gogul Balakrishnan and Thomas Reps
Model Checking-Based Genetic Programming with Application to Mutual Exclusion
Gal Katz and Doron Peled

Programme of Tuesday, April 1

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

MODEL CHECKING II (room: Star)
Conditional probabilities over probabilistic and nondeterministic systems
Miguel Andres and Peter van Rossum
On Automated Verification of Probabilistic Programs
Axel Legay, Andrzej Murawski, Joel Ouaknine and James Worrell
Symbolic Model Checking of Hybrid Systems using Template Polyhedra
Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic
Fast Directed Model Checking via Russian Doll Abstraction
Sebastian Kupferschmid, Joerg Hoffmann and Kim Larsen

12:30 - 14:30 Lunch

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

STATIC ANALYSIS (room: Star)
A SAT based approach to size change termination with global ranking functions
Amir Ben-Amram and Michael Codish
Efficient Automatic STE Refinement Using Responsibility
Hana Chockler, Orna Grumberg and Avi Yadgar
Reasoning Algebraically About P-solvable Loops
Laura Kovacs
On local reasoning in verification
Carsten Ihlemann, Swen Jacobs and Viorica Sofronie-Stokkermans

16:30 - 17:00 Coffee

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

CONCURRENT/DISTRIBUTED SYSTEMS (room: Star)
Interprocedural Analysis of Concurrent Programs Under a Context Bound
Akash Lal, Tayssir Touili, Nicholas Kidd and Thomas Reps
Context-bounded analysis of concurrent queue systems
Salvatore La Torre, Madhusudan Parthasarathy and Gennaro Parlato
On Verifying Fault Tolerance of Distributed Protocols
Dana Fisman, Orna Kupferman and Yoad Lustig

Programme of Wednesday, April 2

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

Unifying Invited Talk (room: Europa)
Verification of higher-order computation: a game-semantic approach
Luke Ong

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

Unifying Invited Talk (room: Europa)
WYSINWYX: What You See Is Not What You eXecute
Tom Reps

15:30 - 16:30 SESSION 3B (TACAS, Wednesday)

TOOLS I (room: Star)
The Real-Time Maude Tool
Peter Olveczky and Jose Meseguer
Z3: An Efficient SMT Solver
Leonardo de Moura and Nikolaj Bjorner
Computation and visualisation of phase portraits for model checking SPDIs
Gordon Pace and Gerardo Schneider
GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan and Chi-Jian Luo

16:30 - 17:00 Coffee

17:00 - 18:30 SESSION 4 (TACAS, Wednesday)

SYMBOLIC EXECUTION (room: Star)
RWset: Attacking Path Explosion in Constraint-Based Test Generation
Peter Boonstoppel, Cristian Cadar and Dawson Engler
Demand-Driven Compositional Symbolic Execution
Saswat Anand, Patrice Godefroid and Nikolai Tillmann
Peephole Partial Order Reduction
Chao Wang, Zijiang Yang, Vineet Kahlon and Aarti Gupta

Programme of Thursday, April 3

09:00 - 10:00 SESSION 1 (TACAS, Thursday)

Invited Talk (room: Europa)
Hardware Verification: Techniques, Methodology and Solutions
Sharad Malik

10:00 - 10:30 Coffee

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

ABSTRACTION, INTERPOLATION (room: Star)
Efficient Interpolant Generation in Satisfiability Modulo Theories
Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani
Generating Quantified Invariants with an Interpolating Saturation Prover
Keneth McMillan
Accelerating Interpolation-based Model-Checking
Nicolas Caniart,Emmanuel Fleury, Jerome Leroux and Marc Zeitoun
Automatically Refining Abstract Interpretations
Bhargav Gulavani, Supratik Chakraborty, Aditya Nori and Sriram Rajamani

15:30 - 16:30 SESSION 3B (TACAS, Thursday)

TOOLS II (room: Star)
SVISS: Symbolic Verification of Symmetric Systems
Thomas Wahl, Nicolas Blanc and Allen Emerson
RESY: Requirement Synthesis for Compositional Model Checking
Bernd Finkbeiner, Hans-Jorg Peter and Sven Schewe
Scoot: A tool for static analysis of SystemC models
Nicolas Blanc, Daniel Kroening and Natasha Sharygina

16:30 - 17:00 Coffee

17:00 - 18:30 SESSION 4 (TACAS, Thursday)

TRUST, REPUTATION (room: Star)
Trusted Source Translation of a Total Function Language
Guodong Li and Konrad Slind
Rocket-fast Proof Checking For SMT Solvers
Michal Moskal
SDSIrep: A Reputation System based on SDSI
Javier Esparza, Ahmed Bouajjani, Stefan Schwoon and Dejvuth Suwimonteerabuth

Detailed Programme Information:

ETAPS 2008 | Top | HTML 4.01 | Last Update: 2007-12-27