5th WAVAS with Holik, Lengal, Lin, and Vojnar

5th Workshop on

Automated Verification, Analysis, and Synthesis

Fri. 25 Oct. 2013, 217 Bow-Li Hall, National Taiwan Univ., Taiwan, ROC



Dr. Churn-Jung 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





Facebook with event photos!

Previous WAVAS':

4th WAVAS on Cloud Testing Service on Jun. 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



   WAVAS is held to promote collaborations in the research area of automated verification and analysis.  We are happy to announce the fifth WAVAS featuring several international visitors, including Professor Tomas Vojnar,  Professor Ondrej Lengal, and Dr. Anthony W. Lin. 

  The fifth WAVAS features speeches and invited presentations by our colleagues, 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, game-theoretical techniques, synthesis, regular system verification. 


opening 08:45-09:00 Prof. Sy-Yen Kuo

(Dean, College of EECS, National Taiwan Univ.)

session 1 09:00-10:30

Prof. Tomas Vojnar

(Brno Univ. of Technology)

Byte-Precise Verification of Low-Level List Manipulation

Dr. Yu-Fang Chen

(Academia Sinica)

An Introduction to Automata Learning Algorithms
Dr. Bow-Yaw Wang

(Academia Sinica)

Learning Algorithms for Boolean Functions
Coffee break 10:30-11:00 @
Session 2 11:00-12:00
Prof. Fang Yu

(National Cheng Chi Univ.)

VIS: A Virtualization Introspection System for Securing KVM-based Cloud Platform

Chung-Hao Huang

Prof. Farn Wang

(National Taiwan Univ.)

Supervised and Guided Mining of Linear Properties of Android Applications
Luncheon 12:00-14:00 @
Session 3 14:00-15:15 Ondrej Lengal

(Brno Univ. of Technology)

Fully Automated Shape Analysis Based on Forest Automata

Prof. Lukas Holik

(Brno Univ. of Technology)

Advanced Topics for Forest Automata

Coffee break


Session 4 15:45-17:15 Dr. Anthony W. Lin

(Oxford Univ.)

Parikh Images of Regular Languages: Complexity and Applications
Chiao Hsieh

(National Taiwan Univ. & Academia Sinica)

Verifying Recursive Programs using Verifiers for Sequential Programs

Pin Hsiuan Chen

(National Taiwan Univ)

Tool demonstration: Testing Service for Android devices.


WAVAS thanks the sponsorship of the following affiliations.

Department of Electrical Engineering, National Taiwan University



Institute of Information Science, Academia Sinica



Research Center for Information Technology and Innovation, Academia Sinica




Interested colleagues are welcome to submit their papers or slides to Professor Farn Wang of National Taiwan University at farn@cc.ee.ntu.edu.tw