1st WAVAS with Dr. John Rushby

1st Workshop on Automated Verification, Analysis, and Synthesis

Tuesday 15 February 2011

112 Barry Lam Hall, National Taiwan University, Taiwan, ROC 

Aim:

WAVAS is held to promote international collaborations in the research area of automated verification and analysis.  We are happy to announce the first WAVAS honoring our distinguished lecturer Dr. John Rushby from Stanford Research Institute (SRI).  Dr. Rushby is the Program Director for Formal Methods and Dependable Systems at SRI.  He is famous in his involvement in the project of PVS.  The first WAVAS features invited speeches by Dr. Rushby, invited presentations by our colleagues, luncheon, and coffee breaks. 

Scopes of interest:

Scopes of interests include but are not limited to the following.

Model checking, proof checking, hardware verification, software verification, timed systems, hybrid systems, complexity, game-theoretical techniques, synthesis, regular system verification. 

Contact:

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. 

Program:

opening	09:45-10:00	Prof. Hsu-Chun Yen	Opening
keynote	10:00-11:00	Dr. John Rushby	What is Software Assurance?
Coffee break	11:00-11:30
Session 1	11:30-12:30
		Prof. Yih-Kuen Tsay	Buechi Store: An Open Repository of Buechi Automata
		Prof. Jie-Hong Roland Jiang Mr. Valeriy Balabanov	Resolution Proofs and Skolem Functions in QBF Evaluation and Applications
		Mr. Chih-hong Patrick Cheng	Algorithmic Game Solving - from Theory towards Applications in Synthesis
Luncheon	12:30-14:20
Session 2	14:20-15:40	Prof. Fang Yu	Patching Vulnerabilities with Sanitization Synthesis
		Prof. Tian-Li Yu	GA Road: From pure random to learning and beyond.
		Dr. Yu-Fang Chen Mr. Chih-Duo Hong	A Symbolic Algorithm to Model Check Quantitative Properties of Probabilistic Programs (Work-in-progress)
		Prof. Chung-Yang Ric Huang Mr. Kai-Fu Tang	Interpolation-Based Incremental ECO Synthesis for Multi-Error Logic Rectification
Coffee break	15:40-16:10
Session 3	16:10-17:30	Prof. Pao-Ann Hsiung	Learning-based Assume-Guarantee Synthesis
		Dr. Shin-Cheng Mu	Algebra of Programming in Agda
		Prof. Farn Wang Ms. Su-Feng Cindy Li	Model-Based GUI Testing
		Prof. Farn Wang Mr. Jung-Hsuan Wu	Evolving a test oracle in black-box testing

WAVAS thanks the sponsorship of the Department of Electrical Engineering, National Taiwan University. 

John Rushby received B.Sc. and Ph.D. degrees in computing science from the University of Newcastle upon Tyne in 1971 and 1977, respectively. He joined the Computer Science Laboratory of SRI International in 1983, and served as its director from 1986 to 1990. Since 1990, he has managed its research program in formal methods and dependable systems; this program is responsible for the PVS verification system, the SAL model checkers, and the ICS decision procedures. He was selected as an SRI Fellow in 2004. Prior to joining SRI, he held academic positions at the Universities of Manchester and Newcastle upon Tyne in England. His research interests center on the use of formal methods for problems in the design and assurance of dependable systems. Dr. Rushby is a member of the IEEE, the Association for Computing Machinery, the American Institute of Aeronautics and Astronautics, and the American Mathematical Society. He is a former associate editor for Communications of the ACM, IEEE Transactions on Software engineering, and Formal Aspects of Computing. He is the author of the (now rather outdated) chapter on formal methods for the FAA Certification Handbook.