Abstract State Machines: Title Index

---

[A]

• "The ABCs of Specification: AsmL, Behavior, and Components"
• "An Abstract Communication Model"
• "An Abstract State Machine Primer"
• "Abstract State Machine Semantics of SDL"
• "An Abstract State Machine Specification and Verification of the Location Consistency Memory Model and Cache Protocol"
• "An Abstract State Machine specification of the DEC-Alpha Processor Family"
• "Abstract State Machines Capture Parallel Algorithms"
• "Abstract State Machines Capture Parallel Algorithms: Correction and Extension"
• "Abstract State Machines: A Method for High-Level System Design and Analysis"
• "Abstract State Machines: A Unifying View of Models of Computation and of System Design Frameworks"
• "Abstract State Machines 1988-1998: Commented ASM Bibliography"
• "Abstract state machines and computationally complete query languages"
• "Abstract State Machines and Pure Mathematics"
• "Algebraic Operational Semantics and Occam"
• "Algebraic Specification of Dynamic Objects"
• "Algorithms vs. Machines"
• "The ASM Refinement Method"
• "An ASM-Based Approach for Mobile Systems"
• "ASM-Based Mechanized Verification of Compiler Back-Ends"
• "An ASM Dynamic Semantics for Standard ML"
• "An ASM Dynamic Semantics for Standard ML" (Extended Abstract)
• "The ASM Ground Model Method as a Foundation of Requirements Engineering"
• "An ASM Implementation of a Self-Applicable Partial Evaluator"
• "An ASM Macro Language for Sets"
• "The ASM Refinement Method"
• "An ASM Semantics for UML Activity Diagrams"
• "An ASM Specification of the Operational Semantics of MIS"
• "Automatic Verification of Abstract State Machines"
• "An Automatic Verification Tool for UML"

---

[B]

• "Background, Reserve, and Gandy Machines"
• "The Bakery Algorithm: Yet Another Specification And Verification"
• "Broy-Lamport Specification Problem: A Gurevich Abstract State Machine Solution."

---

[C]

• "Capturing Requirements by Abstract State Machines: The Light Control Case Study"
• "A Case Study on Model Checking and Refinement of Abstract State Machines"
• "Choiceless Polynomial Time"
• "CLAM specification for provably correct compilation of CLP(R) programs"
• "Combining Abstract State Machines with Predicate Transition Nets"
• "Communicating evolving algebras."
• "A Compiler Correctness Proof for the Static Link Technique by means of Evolving Algebras"
• "Compiling Abstract State Machines to C++"
• "Compiling Abstract State Machines to C++ (Extended Abstract)"
• "Completeness of a Bytecode Verifier and a Certifying Java-to-JVM Compiler"
• "Complex Transitions in Evolving Algebras"
• "Composition and Submachine Concepts for Sequential ASMs"
• "Computation and Specification Models: A Comparative Study"
• "Computer-Aided Analysis and Validation of Heterogeneous System Specifications"
• "Conformance Checking of Components Against Their Non-deterministic Specifications"
• "The Constrained Shortest Path Problem: A Case Study in Using ASMs"
• "Contracts, Components, and their Runtime Verification on the .NET Platform"
• "Cooperation Contracts"
• "Correctness of compiling Occam to Transputer code"
• "A correctness proof for pipelining in RISC architectures"
• "Correctness proof for the WAM with types"
• "Correctness proof of a Distributed Implementation of Prolog by means of Abstract State Machines"
• "Coverage-Driven Automated Compiler Test Suite Generation"

---

[D]

• "Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation."
• "Definition of a Parallel Execution Model with Abstract State Machines".
• "Deriving Partial Correctness Logics From Evolving Algebras"
• "Description and Simulation of Microprocessor Instruction Sets Using ASMs"
• "A Description of the Tableau Method Using Abstract State Machines"
• "Design for Reuse via Structuring Techniques for ASMs."
• "Developing Efficient Interpreters Based on Formal Language Specifications."
• "Dynamic Interpretations of Constraint-Based Grammar Formalisms"

---

[E]

• "Encoding Abstract State Machines in PVS"
• "Enhanced Control Flow Graphs in Montages"
• "Equivalence Is In The Eye Of The Beholder"
• "An Evolving Algebra Abstract Machine"
• "The Evolving Algebra Semantics of COBOL. Part 1: Programs and Control."
• "Evolving Algebras" (Gurevich)
• "Evolving Algebras" (Visser)
• "Evolving Algebras 1993: Lipari Guide"
• "Evolving Algebras: An Attempt to Discover Semantics"
• "Evolving algebras and labelled deductive systems for the semantic network based reasoning"
• "Evolving Algebras and Mathematical Models of Language"
• "Evolving Algebras and Partial Evaluation"
• "Evolving Databases: An Application to Electronic Commerce"
• "Executable Specifications based on Dynamic Algebras"
• "Extending Dynamic Logic for Reasoning about Evolving Algebras"

---

[F]

• "Fast Dynamic Analysis of Complex HW/SW-Systems based on Abstract State Machine Models"
• "Formal Analysis of the Kerberos Authentication System"
• "Formal Aspects of and Development Environments for Montages"
• "Formal Definition of an Abstract VHDL'93 Simulator By EA-Machines"
• "The Formal Definition of Anlauff's eXtensible Abstract State Machines"
• "Formal design of an abstract machine for constraint logic programming".
• "A Formal Framework for Defining Grid Systems"
• "A formal method for provably correct composition of a real-life processor out of basic components (The APE100 Reverse Engineering Study)"
• "A formal method for provably correct composition of a real-life processor out of basic components (The APE100 Reverse Engineering Study)" (Extended Abstract)
• "A Formal Representation of Abstract State Machines Using PVS"
• "A Formal Semantics for Verilog-VHDL Simulation Interoperability by Abstract State Machine"
• "A Formal Semantics on Net Delay in Verilog-HDL">
• "The Formal Specification of Oberon"
• "A formal specification of Parlog."
• "The Formal Specification of the Interactive Abstract State Machine Language"
• "A formal specification of the PVM architecture."
• "Formal Verification of ASM Designs using the MDG Tool"
• "Formal Verification of ASM Designs using the MDG Tool"
• "Formalization and Application of a Unifying Model for Name Management"
• "A Formalization of Evolving Algebras"
• "Formalizing Database Recovery"

---

[G]

• "Generating an Action Notation Environment from Montages Descriptions"
• "Generating Finite State Machines from Abstract State Machines"
• "Generic Facilities in Object-Oriented ASMs"
• "Grammar Formalisms Viewed As Evolving Algebras"
• "Group Membership Protocol: Specification and Verification"
• "Gurevich Abstract State Machines and Schönhage Storage Modification Machines"

---

[H]

• "Harmonizing Design Languages with Object-Oriented Extensions and an Executable Semantics"
• "The Hidden Computation Steps of Turbo Abstract State Machines"
• "Hierarchical Microprocessor Design Using XASM"
• "High Level System Design and Analysis using Abstract State Machines"
• "Hybrid Abstract State Machines: Using the Hyperreals for Describing Continuous Changes in a Discrete Notation"

---

[I]

• "Implementation of Dynamic Algebras with an Application to Prolog"
• "Initialization Problems for Java"
• "Integrating ASMs into the Software Development Life Cycle"
• "Integrating Domain Specific Language Design in the Software Life Cycle"
• "Integration of the Statecharts in Specware and Aspects of Correct Oberon Code Generation"
• "Interacting Abstract State Machines" (Maia, Iorio, and Bigonha)
• "Interacting Abstract State Machines" (Schönfeld)
• "Interfacing Abstract State Machines with Multiway Decision Graphs"
• "Interfacing ASM with the MDG Tool"
• "Investigating Java Concurrency using Abstract State Machines"

---

[J]

• "Java and the Java Virtual Machine"
• "Java bytecode verification is not possible (Extended Abstract)"

---

[K]

• "Kermit: Specification and Verification"

---

[L]

• "leanEA: A Lean Evolving Algebra Compiler"
• "The Linear Time Hierarchy Theorems for Abstract State Machines and RAMs"
• "Logic + control revisited: an abstract interpreter for Goedel programs."
• "The Logic of Choice"
• "A Logic for Abstract State Machines"
• "A Logic for Abstract State Machines" (Extended Abstract)
• "Logic Programming: The Evolving Algebra Approach"
• "Logician in the Land of OS: Abstract State Machines at Microsoft"
• "Logspace Reducibility via Abstract State Machines"

---

[M]

• "Mapping Automata: Simple Abstract State Machines"
• "A mathematical definition of full Prolog"
• "The mathematics of set predicates in Prolog."
• "May 1997 Draft of the ASM Guide"
• "Metafinite Model Theory"
• "Model Checking Abstract State Machines"
• "Model Checking Abstract State Machines and Beyond"
• "Model Checking for Abstract State Machines"
• "Model Checking Support for the ASM High-Level Language"
• "A model for mathematical analysis of functional logic programs and their implementations."
• "Modeling Cache Coherence Protocol - A Case Study with FLASH"
• "Modeling Rule-Based and Structured Systems with Evolving Algebras"
• "Modelling and Analysis of Distributed and Reactive Systems using Evolving Algebras"
• "Modular Design for the Java Virtual Machine Architecture"
• "Montages: Specifications of Realistic Programming Languages"

---

[N]

• "A New Dynamic Equation Scheduling to extend VHDL-AMS"
• "New Zero-One Law and Strong Extension Axioms"

---

[O]

• "Object-based Abstract State Machines"
• "Object-Oriented Abstract State Machines"
• "Occam: Specification and compiler correctness. Part I: Simple mathematical interpreters."
• "An Offline Partial Evaluator for Evolving Algebras."
• "On ASM-Based Specification of Programming Language Semantics and Reusable Correct Compilations">
• "On Gurevich's Theorem on Sequential Algorithms"
• "On Modular Definitions and Implementations of Programming Languages"
• "On Polynomial Time Computation Over Unordered Structures"
• "On Semantics of Algorithms with Continuous Time"
• "On the Formal Semantics of Design Languages: A compilation approach using Abstract State Machines"
• "On the Construction of Correct Compiler Back-Ends: An ASM Approach"
• "On Verification of Refinements of Asynchronous Timed Distributed Algorithms"
• "Operational Semantics of Transactions"
• "The Origins and the Development of the ASM Method for High Level System Design and Analysis"

---

[P]

• "Partial Updates: Exploration"
• "Partially Ordered Runs: A Case Study">
• "A Practical Method for Specification and Analysis of Exception Handling: A Java/JVM Case Study"
• "A Practical Method for Rigourously Controllable Hardware Design."
• "Privacy, Abstract Encryption and Protocols: an ASM Model - Part I"
• "A Programmer Friendly Modular Definition of the Semantics of Java."
• "Programming with Variable Functions"
• "Prototyping Realistic Programming Languages Based Formal Specificiations"

---

[Q]

• "Quantum Computing and Abstract State Machines"

---

[R]

• "The Railroad Crossing Problem: An Experiment with Instantaneous Actions and Immediate Reactions"
• "The Railroad Crossing Problem: Towards Semantics of Timed Algorithms and their Model-Checking in High-Level Languages"
• "A Realistic Environment for Crypto-Protocol Analyses by ASMs"
• "Reasoning about Abstract State Machines: The WAM Case Study"
• "Recursive Abstract State Machines"
• "Refinement of a typed WAM extension by polymorphic order-sorted types"
• "Refining Abstract Machine Specifications of the Steam Boiler Control to Well Documented Executable Code."
• "Refining an ASM Specification of the Production Cell to C++ Code"
• "Remarks on Turbo ASMs for Functional Equations and Recursion Schemes"
• "Report on a Practical Application of ASMs in Software Design"
• "Rich Sequential-Time ASMs"

---

[S]

• "A Self-Applicable Partial Evaluator for ASM"
• "Semantic Analysis of VHDL-AMS by Attribute Grammar"
• "A Semantic Model for the State Machine in the Unified Modeling Language"
• "Semantic Validation of VHDL-AMS by an Abstract State Machine"
• "The Semantics of Behavioral VHDL'93 Descriptions"
• "Semantics of Object-Oriented Data Models -- The Evolving Algebra Approach"
• "The Semantics of the C Programming Language"
• "The Semantics of the C++ Programming Language"
• "The Semantics of the Java Programming Language: Preliminary Version"
• "Semantics of the Process Description Language"
• "Sequential Abstract State Machines Capture Sequential Algorithms"
• "A Sound and Complete SOS-Semantics for Non-Distributed Deterministic Abstract State Machines"
• "Specification and correctness proof of a WAM extension with abstract type constraints"
• "Specification and Optimization of the Smalltalk programs"
• "Specification and Verification of Pipelining in the ARM2 RISC Microprocessor"
• "Specification and Verification of Pipelining in the ARM2 RISC Microprocessor (Extended Abstract)"
• "Specification and verification of the Windows Card runtime environment using Abstract State Machines"
• "Specification of an Oberon Compiler by Means of a Typed Gurevich Machine"
• "Specification of Dynamic Systems by Typed Gurevich Machines"
• "Specification, Simulation and Testing of COM Components using Abstract State Machines"
• "Specifications in-the-Large by Typed ASMs"
• "Specifying Algorithms Using Evolving Algebra. Implementation of Functional Programming Languages."
• "Specifying Complex and Structured Systems with Evolving Algebras"
• "Spying on Components: A Runtime Verification Technique"
• "State-based Semantics of a Pascal-like Language"
• "The Static and Dynamic Semantics of C"
• "Stepwise Refinement of an Abstract State Machine for WHNF-Reduction of lambda-Terms"
• "Strong Extension Axioms and Shelah's Zero-One Law for Choiceless Polynomial Time"
• "Structural Simulation Proofs based on ASMs even for Non-Terminating Programs"
• "A Structured Presentation of a Closure-Based Compilation Method for a Scoping Notion in Logic Programming"
• "Supporting Abstraction when Model Checking ASM"
• "Synthesizing ASMs from Natural Language Requirements"
• "Systems Level Specification and Modelling of Reactive Systems: Concepts, Methods, and Tools"

---

[T]

• "Table ASMs"
• "A Termination Detection Algorithm: Specification and Verification"
• "Testing with Abstract State Machines"
• "A Theory of Many-sorted Evolving Algebras"
• "Tool Support for Language Design and Prototyping with Montages"
• "A Toolset for Supporting UML Static and Dynamic Model Check"
• "Toward Industrial Strength Abstract State Machines"
• "Towards a Mathematical Specification of a Graph-Narrowing Machine"
• "Towards a mathematical specification of the APE100 architecture: the APESE model"
• "Towards a Methodology for Model Checking ASM: Lessons learned from the FLASH Case Study"
• "Towards a Unified Analysis Methodology of HW/SW Systems based on Abstract State Machines: Modelling of Instruction Sets"
• "Towards an Action Refinement Calculus for Abstract State Machines"
• "Towards Comprehensive Tool Support for Abstract State Machines: The ASM Workbench Tool Environment and Architecture"
• "Transformations of Evolving Algebras"
• "Typed Gurevich Machines Revisited"

---

[U]

• "Universal Plug and Play Machine Models"
• "Using Abstract State Machines at Microsoft: A Case Study"
• "Using ASM specification for automatic test suite generation for mpC parallel programming language compiler"

---

[V]

• "A Validation Method for a UML Model Based on Abstract State Machines"
• "Verification of ASM Refinements Using Generalized Forward Simulation"
• "Verification of Relational Transducers for Electronic Commerce"
• "Verification of Timed Algorithms: Gurevich Abstract State Machines versus First Order Timed Logic"

---

[W]

• "The WAM - definition and compiler correctness."
• "Why Use Evolving Algebras for Hardware and Software Engineering?"

---

[X]

• "XASM -- An Extensible, Component-Based Abstract State Machines Language"

---

[Y]

No papers in this category.

---

[Z]

No papers in this category.