Tuesday
Wednesday
Thursday
KEYNOTE SPEAKERS:
Thomas Ball (Microsoft Research, US)
Jin Yang (Intel Corporation, US)
Mihalis Yannakakis (Columbia University. US)
INVITED TUTORIALS:
Three tutorials on software verification, hardware verification and the theory of verification will be given by the three keynote speakers T. Ball, J. Yang and M. Yannakakis, respectively.
IMPORTANT DATES:
20 May 2006, submission deadline
10 July 2006, acceptance notification
1 August 2006, camera-ready copy
23 October - 26 October 2006, ATVA 2006
PUBLICATION:
Following ATVA 2004 (LNCS 3299) and ATVA 2005 (LNCS 3707), the formal proceedings is to be published as a volume of LNCS, Springer-Verlag.
Extended versions of selected papers on theoretical foundation and technology-transfer from the conference series will be solicited for publication in special issues of the International Journal of Foundations of Computer Science (IJFCS) (http://www.cs.ucsb.edu/~ijfcs) and of the International Journal on Software Tools for Technology Transfer
(STTT)
(http://sttt.cs.uni-dortmund.de).
FOCUS:
ATVA 2006 is the fourth in the series of symposia on Automated Technology for Verification and Analysis. 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. Submissions reporting original contributions are solicited in all
areas of automated verification and analysis.
SCOPE:
The scope of interest is intentionally kept broad; it includes:
(1) theory useful for providing designers with automated support
for obtaining correct software or hardware systems, including
both functional and non functional aspects, such as: theory
on (timed) automata, Petri-nets, concurrency theory, compositionality,
model-checking, automated theorem proving, synthesis,
performance analysis, correctness-by-construction results,
infinite state systems, abstract interpretation, decidability results,
parametric analysis or synthesis.
(2) applications of theory in engineering methods and particular
domains and handling of practical problems occurring in tools,
such as: analysis and verification tools, synthesis tools,
reducing complexity of verification by abstraction, improved
representations, handling user level notations (such as UML), practice
in industry 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. Of particular interest are algorithms on one hand and methods and tools for integrating formal approaches into industrial practice. Special care should be taken as we