7th Workshop on Automated Verification, Analysis, and Synthesis

Tuesday 20 October 2015

213 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




Previous WAVAS':

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 


   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 real-world projects. 

  The 7th WAVAS features 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.  

Call for Submissions:

For all interested authors, please submit your papers to the general co-chairs.   Submissions must be in PDF in IEEE proceeding format with 10 to 15 pages.   For more information on typesetting, please check



09:45-10:00 Prof. Farn Wang (NTU) Opening
10:00-11:00 Dr. Churn-Jung Liau (Academia Sinica)

A Logic for Reasoning about Justified Uncertain Beliefs

11:00-11:30 Coffee Break
Kuan-Hua Tu (NTU) QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving

Chun-Han Lin and Prof. Fang Yu (NCCU)

Space Connection: A New 3D Tele-Immersion Platform for Web-Based Gesture-Collaborative Games and Services

12:30-14:00 Lunch 
14:00-15:30 Tsung-Ju Lii (NTU) PAC Learning-Based Verification and Model Synthesis
Dr. Ming-Hsien Tsai (Academia Sinica)

Verifying Curve25519 Software

Shu-Wei Huang and Prof. Fang Yu (NCCU) Behavior-Aware Recommendation of iOS Mobile Applications

Coffee Break

16:00-17:00 Chi-Yun Wu (NTU) Automated Testing of Web Applications with Text Input

Shang-Yi Huang (NTU)

ABCA: Android Black-Box Coverage Analyzer of Mobile Apps without Source Code


WAVAS thanks the sponsorship of the following affiliations.

Department of Electrical Engineering, National Taiwan University


Institute of Information Science, 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