This book constitutes the refereed proceedings of the Second International Conference on Automated Technology for Verificaton and Analysis, ATVA 2004, held in Taipei, Taiwan in October/November 2004.

The 24 revised full papers presented together with abstracts of 6 invited presentations and 7 special track papers were carefully reviewed and selected from 69 submissions. Among the topics addressed are model-checking theory, theorem-proving theory, state-space reduction techniques, languages in automated verification, parametric analysis, optimization, formal performance analysis, real-time systems, embedded systems, infinite-state systems, Petri nets, UML, synthesis, and tools.