What's New: Abstract State Machines 1997

22 December 1997

• Added the following papers:
  • A paper describing EvADE, a compiler/run-analyzer for ASMs written in Gofer. (See also the EvADE Home Page.)
  • A paper describing a Scheme-based interpreter for ASMs.
• Updated the paper describing transformations on ASMs.

19 December 1997

• Added the following papers:
  • A continuation of a discussion of continuous-time logics and the railroad crossing problem.
  • A semantic analysis for VHDL-AMS, a mixed-signal extension of VHDL.
  • A discussion of the use of ASMs for systems level specification.
  • A specification of a compiler for Oberon.
  • An ASM specification of the DEC-Alpha processor family.
  • A specification of the notion of dynamic objects using ASMs.
  • A presentation of EDL, an extended dynamic logic suitable for reasoning about ASMs.
  • A presentation of FLEA, a multi-modal language for ASMs, and its relationship to modal logics.

18 December 1997

• Added links for the 5th International ASM Workshop.
• Did some miscellaneous clean-up, deleting some outdated papers.
• Added the following papers:
  • An approach for specifying complex structured systems with ASMs by means of aggregation and composition.
  • A comparison of ASMs with predicate transition nets.
  • An application of ASMs to present the high-level semantics for MIR, an AI semantic network system.
  • A description of Montages and the Gem-Mex tool.
• Updated the paper on model checking and the railroad crossing problem.

9 October 1997

• Added an extended abstract for the verification of pipelining in the ARM microprocessor.
• Fixed some miscellaneous missing/broken/outdated references.

18 September 1997

• Added a paper describing a structural operational and an axiomatic semantics for ASMs.
• Added a paper describing an algorithm for finding the weak head normal form (WHNF) of an arbitrary term in the lambda-calculus.
• Added a paper describing the tableau calculus for first-order predicate logic, using ASMs.
• A couple of recent papers "disappeared" from the site due to disk problems on our FTP site; all should be fixed now. If you still can't access something, please send e-mail to huggins@acm.org. Thanks.

25 August 1997

• Fixed the link to the paper on evolving databases.

7 August 1997

• Added a paper describing evolving databases (a database model based on ASMs, formerly "evolving algebras") to the database page.
• Added a paper describing an ASM for the control constructs of COBOL to the programming languages page.
• Added a search page.

17 July 1997

• Added a link for GEM: Graphical Editor for Montages to the WWW/FTP page.
• Added the paper on the bakery algorithm to the real-time page.

4 June 1997

• Updated the bibliographic references to the following papers:
  • A specification and verification of the pipelined DLX microprocessor.
  • A presentation of the salient features of ASMs, as part of a discussion of the use of ASMs in the design and analysis of hardware and software systems.
  • A discussion on equivalence and inequivalence.

31 May 1997

• Added links to the FZI Production Cell Control Problem and Alfonso Pierantonio's pages on Montages to the WWW/FTP links page.
• Added a new page dealing with mechanical verification applied to ASM specifications.
• Added the following paper which appeared in Journal of Universal Computer Science, vol. 3, no. 4 (courtesy of Springer-Verlag):
  • A mechanical verification of the Börger and Rosenzweig hierarchy of ASMs refining Prolog to WAM.
• Added/updated the following papers which appeared in Journal of Universal Computer Science, vol. 3, no. 5 (courtesy of Springer-Verlag):
  • A discussion of Montages, a version of ASMs tailored for specifying static and dynamic semantics of programming languages.
  • A presentation of the syntax, static, and dynamic semantics of Oberon.
  • An approach for producing provably corrent compiler back-ends.
  • A specification and proof of correctness for the Prolog Distributed Processor (PDP), a WAM extension for parallel execution of Prolog on distributed memory.
  • A demonstration of the complete software development life cycle applied to the FZI production cell control problem, including the refinement to the level of C++ code.
  • The use of the model checker SMV to verify ASM models (in particular, the production cell control model).

29 May 1997

• Added new pages dealing with abstract algorithms and other models of computation in comparison/conjunction with ASMs.
• Added/updated the following papers which appeared in Journal of Universal Computer Science, vol. 3, no. 4 (courtesy of Springer-Verlag):
  • A description of recursive ASMs.
  • The linear time hierarchy theorems for abstract state machines and RAMs.
  • A demonstration of the equivalence of Schönhage storage modification machines and ASMs.
  • A specification, refinement, and verification of an algorithm for the constrained shortest path problem.
  • A specification and verification of algorithms for database recovery.
  • A presentation of a compilation method for scoping in logic programming.
• Updated the paper on typed ASMs (the previous version was formatted for A4 paper; this version is now formatted for US letter paper).

28 May 1997

• Added a link to the second special issue on ASMs in the Journal of Universal Computer Science to the WWW/FTP page.
• Made some major changes in appearance, notably the addition of frames (as well as non-frame alternatives) and reworking some of the navigational links. Again, if you find something has broken in the process, please e-mail huggins@acm.org. (Thanks.)

26 May 1997

• Added a paper on choiceless polynomial time using ASMs.
• Added an updated paper on typed ASMs.
• Made subtle HTML changes to most of the pages on this site to make them more HTML-compliant (using weblint). The changes should be invisible to most browsers; if you find something has broken in the process, please e-mail huggins@acm.org. (Thanks.)

19 May 1997

• The 1997 ASM Guide is now available as WWW pages.

15 May 1997

• Added a paper on concurrent computation within the ASM framework.

13 May 1997

• The May 1997 Draft of the ASM Guide is now available.

12 May 1997

• Added a link to the recent special issue on ASMs in the Journal of Universal Computer Science to the WWW/FTP page.

8 May 1997

• Added an early paper on distributed ASMs and Occam.
• Updated the paper on the bakery algorithm.
• Updated the reference to the paper on the correctness of the static link technique (used in stack-based implementations of imperative programming languages).
• Added a link to the steam-boiler control specification problem to the WWW/FTP sites page.

4 March 1997

• Added a paper on the semantics of Oberon.

27 February 1997

• Added a page on hardware applications, and copied over various papers concerning hardware.

25 February 1997

• Added a link to the Formal Methods Europe Applications Database (http://www.csr.ncl.ac.uk/projects/FME/InfRes/applications/index.html) to the WWW/FTP site page.

22 February 1997

• Added a page on verification, and copied over various papers which include some sort of verification.
• Added a paper on object-oriented data models.
• Updated the paper on metafinite model theory.
• Updated the paper on cooperation contracts in object-oriented database design (the previous version generated problems printing on US-letter paper.)

7 February 1997

• Added a new version of a paper on database recovery, and removed two older versions of that paper.
• Added a paper on cooperation contracts in object-oriented database design.
• Corrected a minor typographical error in the railroad crossing paper.

6 February 1997

• Added a full paper giving the linear time hierarchy theorems for abstract state machines and RAMs. (The previous paper on this site was an extended abstract.)

18 January 1997

• A draft version of the 1997 ASM Guide is being produced; draft sections (subject to revision!) will be posted on the referenced page as they become available. Please send your comments on the new ASM Guide to Yuri Gurevich.
• Added a paper on a general implementation scheme for CLP(X), based on the WAM and PAM papers.
• Removed an older version of the papers on Protos-L (PAM) (current versions of the papers are of course still available).
• Updated the paper on pipelining in the DLX microprocessor.
• Moved the "what's new" entries for 1996 to a separate page.

What's New for 1996

What's New for 1995