[Om-announce] AVoCS 2014: Final Call for Participation

[Wojciech Mostowski]

(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

-- 
Wojciech Mostowski
University of Twente
Formal Methods and Tools, EWI
EWI-FMT, P.O. Box 217, 7500AE Enschede, The Netherlands
e-mail: w.mostowski at utwente.nl
www: http://wwwhome.ewi.utwente.nl/~mostowskiwi/
tel: +31-53-489 3640
fax: +31-53-489 3247