Cochairs:
Dr.
ChurnJung Liau
Inst. of Information Science,
Academia Sinica
¡@
Prof.
Farn Wang
Dept.
of Electrical Engineering, National Taiwan University
Local Arrangement Chair:
Prof. Farn Wang
National Taiwan University
¡@
¡@
Registration
Previous WAVAS':
7th WAVAS on Oct. 20, 2015
6th WAVAS with Professor Huimin
LIn on Nov. 28, 2014
5th WAVAS
with
Holik, Lengal, Lin, and Vojnar on Oct. 25, 2013
4th WAVAS on TaaS on
June 28, 2013
3rd
WAVAS with Sven Schewe on Oct. 18, 2012.
2nd WAVAS with
Gerard Holzmann on April 10, 2012.
1st WAVAS with
John Rushby on Feb. 15, 2011¡@ 
Aim:
WAVAS is held to
promote collaborations in the research area of automated verification and
analysis. We are happy to announce the fourth WAVAS featuring the
techniques and opportunities for our verification researchers in the booming
cloud computing. With the gradual convergence of Interactive Development
Environments (IDE) in cloud computing, we can now focus on a few IDEs and expect
our innovation be accessible via those IDEs to the app developers.
Thus the opportunity is better than ever for applying
formal verification technologies to realworld projects.
The
8th WAVAS features invited presentations consist of talks by
Professor Jan Peleska and Professor WenLing Huang, luncheon, and coffee breaks.
Scopes of interest:
Scopes of interests include but are not limited
to the following.
Software testing, model checking,
proof checking, hardware verification, software verification, timed systems,
hybrid systems, complexity, gametheoretical techniques, synthesis, regular
system verification.
Program:
09:0009:05 
Prof.
Farn Wang (NTU) 
Opening 
09:1010:30 
Prof. Jan Peleska
(University
of Bremen and Verified Systems International GmbH) 
Industrial verification of avionic, automotive, and railway
systems practical application and theoretical foundations
(I)
Abstract:
The verification of safetycritical systems requires
considerable effort. For systems of the highest criticality 
such as railway interlocking systems, aircraft engine
controllers, or antilock braking systems in cars  this
verification effort is wellknown to surpass the development
effort, that is, the amount of hours needed to specify, design,
and program the software. Since the complexity of
safetycritical applications continuously increases, their
thorough verification requires automation: otherwise it could
never be performed within the tight financial budgets and time
frames that are typical for such projects. In this presentation
it is highlighted how theoretical foundations in the fields of
mathematics and computer science help to solve this problem 
sometimes in quite a surprising way: mathematical models
originally intended only for increasing the insight into complex
system behaviours have been found to be representable in
computers and exploitable for automated verification purposes.
Starting from practical industrial verification problems, it is
highlighted how automated model checking can be applied to
verifying highly complex system designs involving concurrency
and realtime properties. We show how tests can be automatically
generated from mathematical models, so that the whole process of
test case identification and test procedure programming can be
fully automated, allowing even to prove the correctness of the
system under test, under certain hypotheses.
The material presented in this talk is based on projects
performed by Verified Systems International, a company providing
tools and services for verification and validation of
safetycritical systems. The theoretical foundations have been
elaborated at the University of Bremen, in collaboration with
many research partners worldwide.
¡@ 
10:3011:00 
Coffee Break 
11:0012:20 
Prof. Jan Peleska
(University
of Bremen and Verified Systems International GmbH) 
Industrial verification of
avionic, automotive, and railway systems practical application
and theoretical foundations (II)

12:2014:30

Luncheon 
14:3016:00 
Prof.
WenLing Huang
(University of Hamburg) 
Testing SafetyCritical
Discrete State Systems: Mathematical Foundations and Concrete
Algorithms 
16:0016:30 
¡@ Coffee Break 
16:3018:00 
Prof.
WenLing Huang
(University of Hamburg) 
Testing
InfiniteState Systems: Mathematical Foundations and Concrete
Algorithms 
Sponsors:
WAVAS thanks the sponsorship of the
following affiliations.
Department
of Electrical Engineering,
National Taiwan University.
¡@
Institute
of Information Science, Academia Sinica ¡@ 