AsmL: Abstract State Machine Language

Established: November 2, 2001

Publications

View by:

- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  Publication
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  Publication
- On Bounded Reachability of Programs with Set Comprehensions
  
  Margus Veanes, Ando Saabas
  
  LPAR'08 | November 2008
  
  LPAR'08
  
  Publication
- Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
  
  Margus Veanes, Ando Saabas
  
  ABZ'08 | September 2008
  
  This is an extended abstract.
  
  Publication Publication
- An SMT Approach to Bounded Reachability Analysis of Model Programs
  
  Margus Veanes, Nikolaj Bjørner, Alexander Raschke
  
  FORTE'08 | June 2008
  
  FORTE'08
  
  Publication Project
- Bounded reachability of model programs
  
  Margus Veanes, Ando Saabas, Nikolaj Bjørner
  
  MSR-TR-2008-81 | May 2008
  
  Parts of this report are presented at FORTE'08 and LPAR'08.
  
  Publication
- Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer
  
  Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, Lev Nachmanson
  
  Formal Methods and Testing | Published by Springer Verlag | 2008, Vol 4949
  
  ISBN: 978-3-540-78916-1
  
  The attached file is a preliminary version.
  
  Publication Project Project
- Can Abstract State Machines Be Useful in Language Theory?
  
  Yuri Gurevich, Margus Veanes, Charles Wallace
  
  Theoretical Computer Science | January 2007, Vol 376: pp. 17-29
  
  Publication
- Play to Test
  
  Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
  
  FATES 2005 | July 2005
  
  Publication Project
- Exploration with Multiple State Groupings
  
  Colin Campbell, Margus Veanes
  
  Abstract State Machines 2005 | January 2005
  
  Publication Project
- Partial updates
  
  Yuri Gurevich, Nikolai Tillmann
  
  Theor. Comput. Sci. | January 2005, Vol 336: pp. 311-342
  
  Publication Project
- Semantic essence of AsmL
  
  Yuri Gurevich, Benjamin Rossman, Wolfram Schulte
  
  Theoretical Computer Science | January 2005, Vol 343(3): pp. 370-412
  
  Publication
- Testing Concurrent Object-Oriented Systems with Spec Explorer
  
  Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  January 2005
  
  ISBN: 3-540-27882-6
  
  Publication Project Project
- Abstract Communication Model for Distributed Systems
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  IEEE Transactions on Software Engineering | July 2004, Vol 30(7): pp. 458-472
  
  Publication Project
- Instrumenting Scenarios in a Model-Driven Development Environment
  
  Wolfgang Grieskamp, Nikolai Tillmann, Margus Veanes
  
  Journal of Information and Software Technology | January 2004, Vol 46: pp. 1027-1036
  
  Publication Project Project
- Towards a Tool Environment for Model-Based Testing with AsmL
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  FATES 2003 | January 2004
  
  Publication Project Project
- Serious Specification for Composing Components
  
  Mike Barnett, Wolfgang Grieskamp, Clemens Kerer, Wolfram Schulte, Clemens Szyperski, Nikolai Tillmann, Arthur Watson
  
  Proceedings of the 6th ICSE Workshop on Component-Based Software Engineering: Automated Reasoning and Prediction | May 2003
  
  Publication Project
- Combined Algorithm for Approximating a Finite State Abstraction of a Large System
  
  Rostislav Yavorsky, Margus Veanes
  
  ICSE 2003/Scenarios Workshop | January 2003
  
  ICSE 2003/Scenarios Workshop
  
  Publication Project
- Model-Based Testing with AsmL .NET
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  1st European Conference on Model-Driven Software Engineering | January 2003
  
  Publication Project Project
- Runtime Verification of .NET Contracts
  
  Mike Barnett, Wolfram Schulte
  
  The Journal of Systems and Software | January 2003, Vol 65(3): pp. 199-208
  
  Publication
- Validating Use-Cases with the AsmL Test Tool
  
  Wolfram Schulte, Nikolai Tillmann, Margus Veanes, Mike Barnett
  
  QSIC | January 2003
  
  QSIC
  
  ISBN: 0-7695-2015-4
  
  Publication Project
- Generating finite state machines from abstract state machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  ISSTA 2002 | July 2002
  
  Publication Project
- An Abstract Communication Model
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2002-55 | May 2002
  
  Publication Publication
- High-level Executable Specification of the Universal Plug and Play Architecture
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  HICSS 2002 | January 2002
  
  Publication
- Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines
  
  Uwe Glässer, Margus Veanes
  
  Design and Analysis of Distributed Embedded Systems, IFIP 17th World Computer Congress (DIPES 2002) | January 2002
  
  Publication
- Universal Plug and Play Machine Models
  
  U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2001-59 | June 2001
  
  Publication
- Conformance Testing with Abstract State Machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  EUROCAST 2001 | February 2001
  
  Publication
- The ABCs of Specification: AsmL, Behavior, and Components
  
  Mike Barnett, Wolfram Schulte
  
  Informatica | November 2001, Vol 25(4): pp. 517-526
  
  Publication
- Toward Industrial Strength Abstract State Machines
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  MSR-TR-2001-98 | October 2001
  
  Publication
- Using Abstract State Machines at Microsoft: A Case Study
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes, Mike Barnett
  
  Abstract State Machines | January 2000
  
  Abstract State Machines
  
  ISBN: 3-540-67959-6
  
  Publication

- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  Publication
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  Publication
- Universal Plug and Play Machine Models
  
  U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2001-59 | June 2001
  
  Publication
- Conformance Testing with Abstract State Machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  EUROCAST 2001 | February 2001
  
  Publication
- Using Abstract State Machines at Microsoft: A Case Study
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes, Mike Barnett
  
  Abstract State Machines | January 2000
  
  Abstract State Machines
  
  ISBN: 3-540-67959-6
  
  Publication
- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  Publication
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  Publication
- On Bounded Reachability of Programs with Set Comprehensions
  
  Margus Veanes, Ando Saabas
  
  LPAR'08 | November 2008
  
  LPAR'08
  
  Publication
- An SMT Approach to Bounded Reachability Analysis of Model Programs
  
  Margus Veanes, Nikolaj Bjørner, Alexander Raschke
  
  FORTE'08 | June 2008
  
  FORTE'08
  
  Publication Project
- Bounded reachability of model programs
  
  Margus Veanes, Ando Saabas, Nikolaj Bjørner
  
  MSR-TR-2008-81 | May 2008
  
  Parts of this report are presented at FORTE'08 and LPAR'08.
  
  Publication
- Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer
  
  Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, Lev Nachmanson
  
  Formal Methods and Testing | Published by Springer Verlag | 2008, Vol 4949
  
  ISBN: 978-3-540-78916-1
  
  The attached file is a preliminary version.
  
  Publication Project Project
- Can Abstract State Machines Be Useful in Language Theory?
  
  Yuri Gurevich, Margus Veanes, Charles Wallace
  
  Theoretical Computer Science | January 2007, Vol 376: pp. 17-29
  
  Publication
- Play to Test
  
  Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
  
  FATES 2005 | July 2005
  
  Publication Project
- Partial updates
  
  Yuri Gurevich, Nikolai Tillmann
  
  Theor. Comput. Sci. | January 2005, Vol 336: pp. 311-342
  
  Publication Project
- Exploration with Multiple State Groupings
  
  Colin Campbell, Margus Veanes
  
  Abstract State Machines 2005 | January 2005
  
  Publication Project
- Semantic essence of AsmL
  
  Yuri Gurevich, Benjamin Rossman, Wolfram Schulte
  
  Theoretical Computer Science | January 2005, Vol 343(3): pp. 370-412
  
  Publication
- Testing Concurrent Object-Oriented Systems with Spec Explorer
  
  Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  January 2005
  
  ISBN: 3-540-27882-6
  
  Publication Project Project
- Instrumenting Scenarios in a Model-Driven Development Environment
  
  Wolfgang Grieskamp, Nikolai Tillmann, Margus Veanes
  
  Journal of Information and Software Technology | January 2004, Vol 46: pp. 1027-1036
  
  Publication Project Project
- Towards a Tool Environment for Model-Based Testing with AsmL
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  FATES 2003 | January 2004
  
  Publication Project Project
- Serious Specification for Composing Components
  
  Mike Barnett, Wolfgang Grieskamp, Clemens Kerer, Wolfram Schulte, Clemens Szyperski, Nikolai Tillmann, Arthur Watson
  
  Proceedings of the 6th ICSE Workshop on Component-Based Software Engineering: Automated Reasoning and Prediction | May 2003
  
  Publication Project
- Combined Algorithm for Approximating a Finite State Abstraction of a Large System
  
  Rostislav Yavorsky, Margus Veanes
  
  ICSE 2003/Scenarios Workshop | January 2003
  
  ICSE 2003/Scenarios Workshop
  
  Publication Project
- Validating Use-Cases with the AsmL Test Tool
  
  Wolfram Schulte, Nikolai Tillmann, Margus Veanes, Mike Barnett
  
  QSIC | January 2003
  
  QSIC
  
  ISBN: 0-7695-2015-4
  
  Publication Project
- Runtime Verification of .NET Contracts
  
  Mike Barnett, Wolfram Schulte
  
  The Journal of Systems and Software | January 2003, Vol 65(3): pp. 199-208
  
  Publication
- Model-Based Testing with AsmL .NET
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  1st European Conference on Model-Driven Software Engineering | January 2003
  
  Publication Project Project
- Generating finite state machines from abstract state machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  ISSTA 2002 | July 2002
  
  Publication Project
- An Abstract Communication Model
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2002-55 | May 2002
  
  Publication Publication
- Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines
  
  Uwe Glässer, Margus Veanes
  
  Design and Analysis of Distributed Embedded Systems, IFIP 17th World Computer Congress (DIPES 2002) | January 2002
  
  Publication
- High-level Executable Specification of the Universal Plug and Play Architecture
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  HICSS 2002 | January 2002
  
  Publication
- The ABCs of Specification: AsmL, Behavior, and Components
  
  Mike Barnett, Wolfram Schulte
  
  Informatica | November 2001, Vol 25(4): pp. 517-526
  
  Publication
- Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
  
  Margus Veanes, Ando Saabas
  
  ABZ'08 | September 2008
  
  This is an extended abstract.
  
  Publication Publication
- Toward Industrial Strength Abstract State Machines
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  MSR-TR-2001-98 | October 2001
  
  Publication
- Abstract Communication Model for Distributed Systems
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  IEEE Transactions on Software Engineering | July 2004, Vol 30(7): pp. 458-472
  
  Publication Project

- Symbolic Bounded Model Checking of Abstract State Machines
  
  Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte
  
  Int J Software Informatics | June 2009, pp. 149-170
  
  Publication
- Can Abstract State Machines Be Useful in Language Theory?
  
  Yuri Gurevich, Margus Veanes, Charles Wallace
  
  Theoretical Computer Science | January 2007, Vol 376: pp. 17-29
  
  Publication
- Partial updates
  
  Yuri Gurevich, Nikolai Tillmann
  
  Theor. Comput. Sci. | January 2005, Vol 336: pp. 311-342
  
  Publication Project
- Semantic essence of AsmL
  
  Yuri Gurevich, Benjamin Rossman, Wolfram Schulte
  
  Theoretical Computer Science | January 2005, Vol 343(3): pp. 370-412
  
  Publication
- Abstract Communication Model for Distributed Systems
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  IEEE Transactions on Software Engineering | July 2004, Vol 30(7): pp. 458-472
  
  Publication Project
- Instrumenting Scenarios in a Model-Driven Development Environment
  
  Wolfgang Grieskamp, Nikolai Tillmann, Margus Veanes
  
  Journal of Information and Software Technology | January 2004, Vol 46: pp. 1027-1036
  
  Publication Project Project
- Runtime Verification of .NET Contracts
  
  Mike Barnett, Wolfram Schulte
  
  The Journal of Systems and Software | January 2003, Vol 65(3): pp. 199-208
  
  Publication
- The ABCs of Specification: AsmL, Behavior, and Components
  
  Mike Barnett, Wolfram Schulte
  
  Informatica | November 2001, Vol 25(4): pp. 517-526
  
  Publication
- Universal Plug and Play Machine Models
  
  U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2001-59 | June 2001
  
  Publication
- Symbolic Bounded Conformance Checking of Model Programs
  
  Margus Veanes, Nikolaj Bjørner
  
  MSR-TR-2009-28 | March 2009
  
  This is an extended version of a paper to appear in PSI'09, LNCS.
  
  Publication
- Bounded reachability of model programs
  
  Margus Veanes, Ando Saabas, Nikolaj Bjørner
  
  MSR-TR-2008-81 | May 2008
  
  Parts of this report are presented at FORTE'08 and LPAR'08.
  
  Publication
- An Abstract Communication Model
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  MSR-TR-2002-55 | May 2002
  
  Publication Publication
- Toward Industrial Strength Abstract State Machines
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  MSR-TR-2001-98 | October 2001
  
  Publication
- Conformance Testing with Abstract State Machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  EUROCAST 2001 | February 2001
  
  Publication
- Using Abstract State Machines at Microsoft: A Case Study
  
  Yuri Gurevich, Wolfram Schulte, Margus Veanes, Mike Barnett
  
  Abstract State Machines | January 2000
  
  Abstract State Machines
  
  ISBN: 3-540-67959-6
  
  Publication
- On Bounded Reachability of Programs with Set Comprehensions
  
  Margus Veanes, Ando Saabas
  
  LPAR'08 | November 2008
  
  LPAR'08
  
  Publication
- Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
  
  Margus Veanes, Ando Saabas
  
  ABZ'08 | September 2008
  
  This is an extended abstract.
  
  Publication Publication
- An SMT Approach to Bounded Reachability Analysis of Model Programs
  
  Margus Veanes, Nikolaj Bjørner, Alexander Raschke
  
  FORTE'08 | June 2008
  
  FORTE'08
  
  Publication Project
- Play to Test
  
  Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
  
  FATES 2005 | July 2005
  
  Publication Project
- Exploration with Multiple State Groupings
  
  Colin Campbell, Margus Veanes
  
  Abstract State Machines 2005 | January 2005
  
  Publication Project
- Testing Concurrent Object-Oriented Systems with Spec Explorer
  
  Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  January 2005
  
  ISBN: 3-540-27882-6
  
  Publication Project Project
- Towards a Tool Environment for Model-Based Testing with AsmL
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  FATES 2003 | January 2004
  
  Publication Project Project
- Serious Specification for Composing Components
  
  Mike Barnett, Wolfgang Grieskamp, Clemens Kerer, Wolfram Schulte, Clemens Szyperski, Nikolai Tillmann, Arthur Watson
  
  Proceedings of the 6th ICSE Workshop on Component-Based Software Engineering: Automated Reasoning and Prediction | May 2003
  
  Publication Project
- Combined Algorithm for Approximating a Finite State Abstraction of a Large System
  
  Rostislav Yavorsky, Margus Veanes
  
  ICSE 2003/Scenarios Workshop | January 2003
  
  ICSE 2003/Scenarios Workshop
  
  Publication Project
- Validating Use-Cases with the AsmL Test Tool
  
  Wolfram Schulte, Nikolai Tillmann, Margus Veanes, Mike Barnett
  
  QSIC | January 2003
  
  QSIC
  
  ISBN: 0-7695-2015-4
  
  Publication Project
- Model-Based Testing with AsmL .NET
  
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes
  
  1st European Conference on Model-Driven Software Engineering | January 2003
  
  Publication Project Project
- Generating finite state machines from abstract state machines
  
  Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
  
  ISSTA 2002 | July 2002
  
  Publication Project
- Universal Plug and Play Machine Models: Modeling with Distributed Abstract State Machines
  
  Uwe Glässer, Margus Veanes
  
  Design and Analysis of Distributed Embedded Systems, IFIP 17th World Computer Congress (DIPES 2002) | January 2002
  
  Publication
- High-level Executable Specification of the Universal Plug and Play Architecture
  
  Uwe Glässer, Yuri Gurevich, Margus Veanes
  
  HICSS 2002 | January 2002
  
  Publication
- Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer
  
  Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, Lev Nachmanson
  
  Formal Methods and Testing | Published by Springer Verlag | 2008, Vol 4949
  
  ISBN: 978-3-540-78916-1
  
  The attached file is a preliminary version.
  
  Publication Project Project

People

Margus Veanes

Principal Researcher

Learn more

Tony Hoare

Emeritus Researcher

Learn more