Programme of TACAS at ETAPS 2008
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:
- Main Conferences:
Complete Programme,
CC,
ESOP,
FASE,
FOSSACS,
TACAS
- Workshops:
ACCAT,
ByteCode,
COCV,
CMCS,
DCC,
FESCA,
FIT,
FORMED,
GALOP,
GT-VMT,
LDTA,
MBT,
MOMPES,
PDMC,
QAPL,
RV,
SafeCert,
SC,
SLA++P,
WGT,
WRLA
ETAPS 2008 |
Top |
HTML 4.01 |
Last Update: 2007-12-27