Abstract State Machines
AbstractThe ASM project started in mid 80s as an attempt to find versatile computing devices able to simulate arbitrary computer systems step-for-step on their natural abstraction levels. The ASM thesis asserts that abstract state machines are such versatile devices. ASMs have been used to construct mathematical models for numerous full-fledged languages (from C to Java, to VHDL, etc.), to validate standard language implementations (e.g. of Prolog, Occam, Java), to verify various real-life (and possibly real-time) distributed (cryptographic and other) protocols, to prove complexity results, etc. See http://www.eecs.umich.edu/gasm in this connection.