[TYPES/announce] AVoCS 2014: Final Call for Participation

[Marieke Huisman]

(Apologies for multiple copies)

**********************************************************************

Call for Participation

14th Automated Verification of Critical Systems (AVoCS) 2014 Workshop

http://www.utwente.nl/avocs2014

24-26th September, 2014

University of Twente, Netherlands

**********************************************************************

Final Call for Participation

The aim of Automated Verification of Critical Systems (AVoCS) 2014 is
to contribute to the interaction and exchange of ideas among members
of the international research community on tools and techniques for
the verification of critical systems. The subject is to be interpreted
broadly and inclusively. It covers all aspects of automated
verification, including model checking, theorem proving, SAT/SMT
constraint solving, abstract interpretation, and refinement pertaining
to various types of critical systems which need to meet stringent
dependability requirements (safety-critical, business-critical,
performance-critical, etc.). Contributions that describe different
techniques, or industrial case studies are encouraged. The technical
programme will consist of invited and contributed talks and also allow
for short presentations of research ideas. The workshop will be
relatively informal, with an emphasis on discussion.

AVoCS topics include (but are not limited to)

Model Checking
Automatic and Interactive Theorem Proving
SAT, SMT or Constraint Solving for Verification
Abstract Interpretation
Specification and Refinement
Requirements Capture and Analysis
Verification of Software and Hardware
Specification and Verification of Fault Tolerance and Resilience
Probabilistic and Real-Time Systems
Dependable Systems
Verified System Development
Industrial Applications

Thanks to Formal Methods Europe (http://www.fmeurope.org/), we offer a
financial support for students registering for AVoCS in the form of a
registration fee waiver (full or partial). Because our financial support
is limited, we ask the students that would like to take the advantage of
this support to submit a short application (deadline August 14th). The
details on how to apply can be found on the AVoCS 2014 webpage
(http://www.utwente.nl/avocs2014).

AVoCS 2014 is coorganised and colocated with SPES_XT Summer School
on Model-based design and analysis of cyber-physical systems:

http://spes2020.informatik.tu-muenchen.de/summerschool2014.html

A registration reduction is offered for participants attending both
events. There are still places free for the prospective summer school
participants.

Important Dates (Early registration expired)

Early registration: 1st September 2014
Workshop: 24-26th September 2014 (2.5 days, ends 26th lunchtime)

Registration and Hotel Details

All the details on how to register and pay are to be found at the
workshop page at
http://fmt.cs.utwente.nl/conferences/avocs2014/register.php.
Hotel information is to be found at
http://fmt.cs.utwente.nl/conferences/avocs2014/local.php

Invited Speakers

The workshop will have three invited speakers:

* Laura Kovács (Chalmers, Sweden) will speak about "Symbol
Elimination for Automated Generation of Program Properties"
Abstract: Automatic understanding of the intended meaning of
computer programs is a very hard problem, requiring intelligence
and reasoning. In this talk we describe applications of our symbol
elimination methods in automated proram analysis. Symbol
elimination uses first-order theorem proving techniques in
conjunction with symbolic computation methods, and derives
nontrivial program properties, such as loop invariants and
loopbounds, in a fully automatic way. Moreover, symbol elimination
can be used as analternative to interpolation for software
verification.

* Alastair Donaldson (Imperial College, U.K.) will speak about "Static
Verification for GPU Kernels"
Abstract: Graphics processing units (GPUs) are nowadays commonly
used to accelerate general purpose computations. Because GPUs are
massively parallel they can be hard to program correctly, and
suffer from concurrency-related defects including data races. In
the GPUVerify project we have been interested in applying static
verification techniques to GPU kernels (the pieces of code that
execute on GPU devices) in order to automatically find or prove
absence of data races. I will describe the method we have designed
to obtain an analysis method for parallel GPU kernels that scales
to large numbers of threads, and will demo the GPUVerify tool in
action on a number of examples. I will then discuss open problems
for research in the area of reliability of data-parallel software.
For an introduction to GPUVerify check out this video:
https://www.youtube.com/watch?v=l8ysBPV8OvA.

This is joint work with current and previous members of the
Multicore Programming Group at Imperial College London, and with
Shaz Qadeer at Microsoft Research.

* Guy Broadfoot (U.K.) will speak about "The highs and lows of
deploying Formal Methods in Industry".
Abstract: I attended my first software conference in 1968; it was
organised by NATO with the title "The Software Crisis." Many of the
papers presented then could have been written yesterday; the
problems of the software industry in producing reliable, correct
software in the face of increasing complexity and shrinking time to
market pressures have not fundamentally changed that much.

In the intervening years as a community we have developed various
tactics for trying to minimise software errors. Advances in theorem
proving and model checking are good examples of systematic efforts
to improve software correctness. Nevertheless, it remains the case
that such approaches are rarely if ever encountered in the
industrial workplace, with the possible exception of some safety
critical domains, such as the software controlling nuclear power
plants.

In spite advances in formal methods and supporting tools, the tools
available to programmers for verifying assertions about program
execution are complex and require knowledge and skills that most
practicing programmers do not have. Formal proofs remain difficult
to construct, especially for anything but the simplest of programs.
Merely constructing assertions to characterise program correctness
is a difficult challenge.

In 1998, I conceived the idea of combing model checking, code
generation and the specification approach of Sequence-based
Specification together to form an integrated software design
platform for developing software components whose design
(implementation) would be formally verified for correctness with
respect to its specification. Other general correctness properties
such as freedom from deadlocks, non-determinism, incomplete cases,
etc. would also be verified. Verification would be performed by
automatically translating Sequence-based specifications into
semantically equivalent CSP process algebra and then applying the
model-checking engine FDR2. After verification was completed,
semantically equivalent source code would be generated in one
of several supported high-level languages.

These ideas were developed further together with Philippa Hopcroft
and in 2003 a company was founded to develop a commercial
implementation of a development platform based on these ideas. In
this talk, I will present an overview of the development platform
and the technologies used. I will then discuss the experience
gained during 10 years of trying to introduce this approach into
industry and the lessons learned along the way.

Research Presentations

The following is the list of full research papers that will be
presented at AVoCS 2014. The complete program is available at
http://fmt.cs.utwente.nl/conferences/avocs2014/program.php

Jan Friso Groote, Remco Van Der Hofstad and Matthias Raffelsieper.
On the Random Structure of Behavioural Transition Systems

Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene.
Using SMT for dealing with nondeterminism in ASM-based runtime
verification

Jingshu Chen, Marie Duflot and Stephan Merz.
Analyzing Conflict Freedom for Multithreaded Programs with Time
Annotations

Morteza Mohaqeqi, Mohammadreza Mousavi and Walid Taha.
Conformance Testing of Cyber-Physical Systems: A Comparative Study

Petr Ročkai, Jiří Barnat and Luboš Brim.
Model Checking C++ with Exceptions

Leo Hatvani, Alexandre David, Cristina Seceleanu and Paul Pettersson.
Adaptive Task Automata with Earliest-Deadline-First Scheduling

Sven Reimer, Matthias Sauer, Paolo Marin and Bernd Becker.
QBF with Soft Variables

Adisak Intana, Michael Poppleton and Geoff Merrett.
A Formal Co-Simulation Approach for Wireless Sensor Network
Development

John Mullins and Béatrice Bérard.
Verification of Information Flow Properties under Rational Observation

Jeremy Sproston.
Exact and Approximate Abstraction for Classes of Stochastic Hybrid
Systems

Ernst Moritz Hahn, Arnd Hartmanns and Holger Hermanns.
Reachability and Reward Checking for Stochastic Timed Automata

Renaud De Landtsheer, Christophe Ponsard, Nicolas Devos, Bénédicte
Moriau and Guy Anckaerts.
A Constraint-Solving Approach for Achieving Minimal-Reset Transition
Coverage of Smartcard Behaviour

Ali Jafari, Ehsan Khamespanah, Marjan Sirjani and Holger Hermanns.
Performance Analysis of Distributed and Asynchronous Systems using
Probabilistic Timed Actors

Steering Committee

Michael Goldsmith, University of Oxford, U.K.
Stephan Merz, INRIA Nancy & LORIA, France
Markus Roggenbach, Swansea University, U.K.

Organization Committee

Marieke Huisman
Wojciech Mostowski (publicity chair)
Jaco van de Pol