Abstract State Machines in Software Development

Margus Veanes

Microsoft Research
Redmond, WA 98052


Abstract State Machines (ASMs) were introduced by Yuri Gurevich, and have provided a foundation for developing a rigorous hardware and software design method which provides abstract high-level system specifications and their stepwise refinement down to the implementations.

During the seminar we will take a look at:
1) The theory of ASMs.
2) The notion of refinement in the context of ASMs.
3) A case study, involving an internal sample program (a debugger) developed at Microsoft.

This talk is for anyone who is interested in the application of Formal Methods in real world software systems.

About myself

I received my MSc, PhL, and PhD degrees from Uppsala University in 1990, 1993, and 1997, respectively. After that I spent 2 years as a postdoc at Max-Planck-Institute in Saarbruecken, Germany, working mainly on decidability a and undecidability issues concerning second-order unification and the guarded fragment of first-order logic.

From July 1999, have been working as a researcher at Microsoft Research in Redmond, USA, in the group "Foundations of Software Engineering" headed by Yuri Gurevich. The main ambition of the group is to make ASMs useful in software development at Microsoft.

ASTEC seminar
Monday, March 27, 2000

Place: Information technology, Uppsala University
Room: 1549
Time: 13.15 - 14.00 (+ coffee and discussion)

Room 1549 is in Building 1, Floor 5, room 49
(in the northern part of the building).

Help on how get here and MIC campus drawing.

There will be an extended period for discussions after the seminar nourished by cookies and coffee.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 1 hour.

Updated 17-Mar-2000 08:28 by Roland Grönroos
e-mail: info -at-    Location: