|
|
Logic & Semantics |
|
|
Logic & Semantics |
Microsoft Research and University of Michigan
gurevich@microsoft.com
The ASM thesis is that every sequential algorithm, on any level of abstraction, can be viewed as a sequential abstract state machine. The thesis inspired diverse applications of ASMs. 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. In the talk, we will justify the sequential ASM thesis by formalizing sequential algorithms, defining sequential ASMs, and then proving that every sequential algorithm can be step-for-step simulated by an ASM. Time permitting, we will illustrate the use of distributed ASMs by proving the correctness of Lamport's Bakery protocol.
