DSSE-TR-2003-2: Proceedings of the 3rd Automated Verification of Critical Systems (AVoCS’03)

DSSE Technical Report DSSE-TR-2003-2

Proceedings of the 3rd Automated Verification of Critical Systems (AVoCS’03)

April 2-3 2003, Southampton (GB)

Michael Leuschel, Stefan Gruner and Stéphane Lo Presti (editors)

`http://www.ecs.soton.ac.uk/~mal/avocs03/`

Automatic Structural Coverage Testing of Java Bytecode
J. Doyle and C. Meudec
A probabilistic coverage for on-the-fly test generation algorithms
N. Goga
Model Checking Multi-Agent Programs with CASP
Rafael H. Bordini, Michael Fischer, Carmen Bardavilla, Willem Visser, and Michael Wooldridge
A Synchronous Bisimulation Based Approach for Information Flow Analysis
Siva Anantharaman and Gaétan Hains
CSP + Clocks: a Process Algebra for Timed Automata
Stefano Cattani and Marta Kwiatkowska
Projection onto State in the Duration Calculus: Relative Completeness
Dimitar P. Guelev and Dang Van Hung
CSP model-checking of liveness properties over eventual delivery networks
William Simmonds
A First Glimpse at Patterns of Data-Independent Induction
M. Goldsmith (and others)
On the expressiveness of CSP refinement checking
Bill Roscoe
Automatic Verification of Real-Time Systems: A case study
Danièle Beauquier, Tristan Crolard, and Evguenia Prokofieva
Compositional CSL model checking for Boucherie product processes
P. Ballarini and J. Hillston
A Hoare Logic for Single-Input Single-Output Continuous-Time Control Systems
Richard J. Boulton, Ruth Hardy, and Ursula Martin
Automated property verification in UML models
Ambrosio Toval, José Sàez, and Francisco Maestre
Robust models for generalized model checking (extended abstract)
Michael Huth
Model Checking Graph Grammars
Arend Rensink
A New encoding and Implementation of Not Necessarily Closed Convex Polyhedra
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella
Deductive Verification of Cache Coherence Protocols
Michael Fischer and Alexei Lisitsa
Modelling Ad hoc On-demand Distance Vector (AODV) Protocol with Timed Automata
Sibusisiwe Chiyangwa and Marta Kwiatkowska
Modelling Ad-hoc Routing Protocols using Game Search: Extended Abstract
Irfan Zakiuddin, Tim Hawkins, Nick Moffat, Sadie Creese, and Chris Leow
Using Probabilistic Model Checking for Dynamic Power Management
Gethin Norman, David Parker, Marta Kwiatkowska, Sandeep Shukla, and Rajesh Gupta
An experiment on synthesis and verification of an industrial process control in the dSL environment
Bram De Wachter, Thierry Massart, and Cédric Meuter
Model Checking Rebeca Code by SMV
M. Sirjani, A. Movaghar, H. Iravanchi, M. Jaghoori, and A. Shali
Feature Integration from a Theory Change Perspective
Hannah Harris and Mark Ryan
Using the extensible model checker XTL to verify StAC Business Specifications
Juan C. Augusto, Michael Leuschel, Michael Butler, and Carla Ferreira

Declarative Systems & Software Engineering Group
Department of Electronics and Computer Science
University of Southampton
Highfield, Southampton SO17 1BJ, United Kingdom