everything is invariant under isomorphisms of structures. (Structures can be viewed as algebras, which explains the original name evolving algebras for ASMs.) The axiomatization and characterization of sequential algorithms have been extended to parallel and interactive algorithms. In the 1990s, through a community effort, the ASM method was developed, using ASMs for the formal specification and analysis (verification and validation) of computer hardware and software. Comprehensive ASM specifications of programming languages (including Prolog, C, and Java) and design languages (UML and SDL) have been developed. A detailed historical account can be found elsewhere. A number of software tools for ASM execution and analysis are available. Publications Books AsmBook: Egon Börger, Robert Stärk. Abstract State Machines: A Method for High-Level System Design and Analysis JBook: R.Stärk, J.Schmid, E.Börger. Java and the Java Virtual Machine: Definition, Verification, Validation Proceedings/Journal Issues (since 2000) 2008: Springer LNCS 5238 Abstract State Machines, B and Z 2007: J.UCS Special Issue with Selected Papers from ASM'07 2006: Springer LNCS 5115 Rigorous Methods for Software Construction and Analysis, ASM and B Dagstuhl Seminar 2005: Fundamenta Informatica Special Issue with Selected Papers from ASM'05 (electronic proceedings) 2004: Springer LNCS 3052 Abstract State Machines 2004 2003: Springer LNCS 2589 Abstract State Machines 2003: Advances in Theory and Practice 2003: TCS special Issue with Selected Papers from ASM'03 2002: Dagstuhl Seminar Report Theory and Applications of Abstract State Machines 2001: J.UCS 7.11 Special Issue with Selected Papers from ASM'01 2000: Springer LNCS 1912 Abstract State Machines: Theory and Applications Comparative case studies with ASM contributions Steam-Boiler Control: Specification Case Study, Springer LNCS 1165 Production Cell: Software Development Case Study, ASM model Railcrossing: Formal Methods for Real-Time Computing, ASM model Light Control: Requirements Engineering Case Study, Dagstuhl Seminar Invoicing: Requirements Capture Case Study Behavioral models for industrial standards OMG for BPMN (version 2006): Springer LNCS 5316 OASIS for BPEL: IJBPMI 1.4 (2006) ECMA for C#: "A high-level modular definition of the semantics of C♯" ITU-T for SDL-2000: formal semantics of SDL-2000 and Formal Definition of SDL-2000 - Compiling and Running SDL Specifications as ASM Models IEEE for VHDL93: E.Boerger, U.Glaesser, W.Mueller. Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines. In: Carlos Delgado Kloos and Peter T.~Breuer (Eds.), Formal Semantics for VHDL, pp. 107–139, Kluwer Academic Publishers, 1995 ISO for Prolog: "A mathematical definition of full Prolog" Tools (in historical order since 2000) ASMETA, the Abstract State Machine Metamodel and its tool