The 7th International Symposium on Automated Technology for Verification and Analysis took place October 14-16, 2009, in Macao. It was organized by United Nations University Inistitute for Software Technology (UNU/IIST) in cooperation with Macau Polytechnic Institute (MPI). It was preceeded by a tutorial day, October 13.
ATVA is one of the important formal methods events in the region and has the stated objective “… to promote research on theoretical and practical aspects of automated analysis, verification and synthesis in East Asia by providing a forum for interaction between the regional and the international research communities and industry in the field.”
About seventy people attended the events, a little less for the tutorials, of which about fifty were registered participants, while the remaining ones were local students and fellows of UNU/IIST. The program for the tutorial day included three in-depth presentations that were eloquently delivered by experts in their respective fields:
- Mathematics, Models, and Methods for Circuit Verification by Professor Mark Greenstreet of Univ. British Columbia, Canada.
- The 2-valued and The 3-Valued Abstraction-Refinement Frameworks in Model Checking by Professor Orna Grumberg of Technion, Israel
- Using FDR to compile and analyse shared variable programs by Professor Bill Roscoe, Oxford University, UK.
The organizers are grateful for the support of FME that helped us to get Mark Greenstreet over.
The tutorial day was an excellent appetizer for the subsequent three days of the regular symposium. It featured three keynotes where the three tutorial speakers gave a perspective and outlook on their respective topics. There was also room for presenting 26 contributed papers which had been selected among 84 submissions. The keynotes and the contributed papers appear as volume 5799 in Lecture Notes in Computer Science by Springer-Verlag.
Zhiming Liu and Anders P. Ravn (co-chairs)
October, 2009