Aims and Objectives

The purpose of ATVA is 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. The past seven events were held in Taiwan (2003-5), Beijing (2006), Tokyo (2007), Seoul (2008) and Macao (2009). The proceedings of ATVA 2010 will be published by Springer as a volume in the LNCS series.

Scope and Topics

The scope of interest is intentionally kept broad; it includes:

• Theories useful for providing designers with automated support for obtaining correct software or hardware systems, including both functional and non functional aspects, such as: theory of (timed and hybrid) automata, process calculi, Petri-nets, concurrency theory, compositionality, model-checking, automated theorem proving, synthesis, performance analysis, correctness-by-construction, infinite state systems, abstract interpretation, decidability results, parametric analysis or synthesis.
  
  
• Applications of theory in engineering methods and other particular domains and handling of practical problems occurring in tools, such as analysis and verification tools, synthesis tools, model transformation tools. Techniques of reducing complexity of verification by abstraction, improved representations. Methods and tools in handling user level notations, such as UML. Practice in industrial applications to hardware, software or real-time and embedded systems. Case studies, illustrating the usefulness of tools or a particular approach are also welcome.

Theory papers should be motivated by practical problems and applications should be rooted in sound theory. We are interested both in algorithms and in methods and tools for integrating formal approaches into industrial practice.