Probabilistic Methods in Verification

Workshop Description and Aims

Scientific Justification: While there has been a steady current of research activity in probabilistic logics and systems for some years, little experimental work has been done up until now. This situation is beginning to change. Randomization has proved effective in deriving efficient distributed algorithms and is now widely used in practical applications, to mention computer networks and graphics. However, randomized algorithms are notoriously difficult to verify: the proofs of their correctness are complex, and therefore argued informally, and thus appropriate formal methods and tools are called for. These have to combine a variety of dissimilar techniques, from conventional proof theory and model checking, through systems modelling to linear algebra and probability theory.

The importance of probabilistic verification lies in the fact that it can provide guarantees that the specifications hold with satisfactory probability in cases when conventional model checking fails, for example when exhaustive search is not feasible due to the size of the system, or when checking `soft deadlines' in real-time systems. It can also be useful in average-case analysis of software and as an abstraction technique.

The central idea for this workshop is to gather researchers working across the whole spectrum of the research activity in probabilistic verification, from semantics and (computational) linear algebra, through randomized algorithms, probabilistic and fuzzy logics, abstract interpretation, to practical experimental work, tools and applications. The workshop's aim is to enable cross-fertilisation of ideas and techniques between areas that are usually not in regular contact through conferences, while at the same time involving research topics of major concern to the LICS community.

Format and agenda: The workshop will be informal and will focus on exchange of information and discussion. It will consist of a number of invited talks on a range of key topics, evenly balanced between theory and applied research, together with a panel session and a number of accepted papers for which submissions are being sought.

Confirmed Speakers

Invited talks
Rajeev Alur, University of Pennsylvania	Model checking of probabilistic real-time systems
Luca de Alfaro, Stanford University, and Tom Henzinger, University of California at Berkeley	Temporal logics for the specification and verification of performance and reliability
Christel Baier, Universitat Mannheim, and Vicky Hartonas-Garmhausen, CMU	Probabilistic Verus: semantic foundations and practical results
Jeremy Gunawardena, BRIMS, Hewlett-Packard	Timing analysis, dynamical systems and exotic linear algebra
Marek Karpinski, University of Bonn	Randomized OBDDs and the model checking
Annabelle McIver, Oxford University	Reasoning about efficiency within a probabilistic mu-calculus
Prakash Panangaden, McGill University	Stochastic techniques in concurrency
Roberto Segala, University of Bologna	Verification of randomized distributed algorithms
K Narayan Kumar, SUNY Stony Brook, Scott Smolka, SUNY Stony Brook, and Rance Cleaveland, North Carolina SU	Infinite Probabilistic and Nonprobabilistic Testing
Moshe Vardi, Rice University	An Automata-Theoretic Approach to Probabilistic Verification
Panel Session
Ed Clarke, CMU, Panel Chair	What tools and theory are needed in order to make probabilistic verification practical?

Submission Guidelines

• Modelling and verification of probabilistic and stochastic systems, including real-time and hybrid systems
• Formal models and verification techniques for randomized algorithms
• Semantics of probabilistic and stochastic processes
• Probabilistic and fuzzy logics
• Design of verification support tools
• Tool demonstrations
• Case studies

Alternatively, authors may instead send 3 copies of the hardcopy of their paper to Marta Kwiatkowska, PC Chair. Each copy should be complete with the author's address including e-mail and FAX, and a short abstract.

All submissions will be refereed in the normal manner. We intend to publish the proceedings of the conference as a volume of Electronic Notes in Theoretical Computer Science to be available at the conference.

Organising Committee and Program Chairs

Local Information