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
Publications
Publications by Year
-
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.
-
On Bounded Reachability of Programs with Set Comprehensions
Margus Veanes, Ando Saabas
LPAR'08 | November 2008
LPAR'08
Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
Margus Veanes, Ando Saabas
ABZ'08 | September 2008
This is an extended abstract.
An SMT Approach to Bounded Reachability Analysis of Model Programs
Margus Veanes, Nikolaj Bjørner, Alexander Raschke
FORTE'08 | June 2008
FORTE'08
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.
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.
-
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
-
Play to Test
Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
FATES 2005 | July 2005
Exploration with Multiple State Groupings
Colin Campbell, Margus Veanes
Abstract State Machines 2005 | January 2005
Partial updates
Yuri Gurevich, Nikolai Tillmann
Theor. Comput. Sci. | January 2005, Vol 336: pp. 311-342
Semantic essence of AsmL
Yuri Gurevich, Benjamin Rossman, Wolfram Schulte
Theoretical Computer Science | January 2005, Vol 343(3): pp. 370-412
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
-
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
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
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
-
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
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
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
Runtime Verification of .NET Contracts
Mike Barnett, Wolfram Schulte
The Journal of Systems and Software | January 2003, Vol 65(3): pp. 199-208
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
-
Generating finite state machines from abstract state machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
ISSTA 2002 | July 2002
An Abstract Communication Model
Uwe Glässer, Yuri Gurevich, Margus Veanes
MSR-TR-2002-55 | May 2002
High-level Executable Specification of the Universal Plug and Play Architecture
Uwe Glässer, Yuri Gurevich, Margus Veanes
HICSS 2002 | January 2002
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
-
Universal Plug and Play Machine Models
U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
MSR-TR-2001-59 | June 2001
Conformance Testing with Abstract State Machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
EUROCAST 2001 | February 2001
The ABCs of Specification: AsmL, Behavior, and Components
Mike Barnett, Wolfram Schulte
Informatica | November 2001, Vol 25(4): pp. 517-526
Toward Industrial Strength Abstract State Machines
Yuri Gurevich, Wolfram Schulte, Margus Veanes
MSR-TR-2001-98 | October 2001
-
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
Publications by Research Area
-
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
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.
-
Universal Plug and Play Machine Models
U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
MSR-TR-2001-59 | June 2001
Conformance Testing with Abstract State Machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
EUROCAST 2001 | February 2001
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
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
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.
On Bounded Reachability of Programs with Set Comprehensions
Margus Veanes, Ando Saabas
LPAR'08 | November 2008
LPAR'08
An SMT Approach to Bounded Reachability Analysis of Model Programs
Margus Veanes, Nikolaj Bjørner, Alexander Raschke
FORTE'08 | June 2008
FORTE'08
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.
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.
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
Play to Test
Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
FATES 2005 | July 2005
Exploration with Multiple State Groupings
Colin Campbell, Margus Veanes
Abstract State Machines 2005 | January 2005
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
Semantic essence of AsmL
Yuri Gurevich, Benjamin Rossman, Wolfram Schulte
Theoretical Computer Science | January 2005, Vol 343(3): pp. 370-412
Partial updates
Yuri Gurevich, Nikolai Tillmann
Theor. Comput. Sci. | January 2005, Vol 336: pp. 311-342
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
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
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
Runtime Verification of .NET Contracts
Mike Barnett, Wolfram Schulte
The Journal of Systems and Software | January 2003, Vol 65(3): pp. 199-208
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
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
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
Generating finite state machines from abstract state machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
ISSTA 2002 | July 2002
An Abstract Communication Model
Uwe Glässer, Yuri Gurevich, Margus Veanes
MSR-TR-2002-55 | May 2002
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
High-level Executable Specification of the Universal Plug and Play Architecture
Uwe Glässer, Yuri Gurevich, Margus Veanes
HICSS 2002 | January 2002
The ABCs of Specification: AsmL, Behavior, and Components
Mike Barnett, Wolfram Schulte
Informatica | November 2001, Vol 25(4): pp. 517-526
-
Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
Margus Veanes, Ando Saabas
ABZ'08 | September 2008
This is an extended abstract.
Toward Industrial Strength Abstract State Machines
Yuri Gurevich, Wolfram Schulte, Margus Veanes
MSR-TR-2001-98 | October 2001
-
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
Publications by Type
-
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
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
Semantic essence of AsmL
Yuri Gurevich, Benjamin Rossman, Wolfram Schulte
Theoretical Computer Science | January 2005, Vol 343(3): pp. 370-412
Partial updates
Yuri Gurevich, Nikolai Tillmann
Theor. Comput. Sci. | January 2005, Vol 336: pp. 311-342
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
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
Runtime Verification of .NET Contracts
Mike Barnett, Wolfram Schulte
The Journal of Systems and Software | January 2003, Vol 65(3): pp. 199-208
The ABCs of Specification: AsmL, Behavior, and Components
Mike Barnett, Wolfram Schulte
Informatica | November 2001, Vol 25(4): pp. 517-526
-
Universal Plug and Play Machine Models
U. Glässer, Y. Gurevich, M. Veanes, Yuri Gurevich, Margus Veanes
MSR-TR-2001-59 | June 2001
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.
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.
An Abstract Communication Model
Uwe Glässer, Yuri Gurevich, Margus Veanes
MSR-TR-2002-55 | May 2002
Toward Industrial Strength Abstract State Machines
Yuri Gurevich, Wolfram Schulte, Margus Veanes
MSR-TR-2001-98 | October 2001
-
Conformance Testing with Abstract State Machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
EUROCAST 2001 | February 2001
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
On Bounded Reachability of Programs with Set Comprehensions
Margus Veanes, Ando Saabas
LPAR'08 | November 2008
LPAR'08
Using Satisfiability Modulo Theories to Analyze Abstract State Machines (Abstract)
Margus Veanes, Ando Saabas
ABZ'08 | September 2008
This is an extended abstract.
An SMT Approach to Bounded Reachability Analysis of Model Programs
Margus Veanes, Nikolaj Bjørner, Alexander Raschke
FORTE'08 | June 2008
FORTE'08
Play to Test
Andreas Blass, Yuri Gurevich, Lev Nachmanson, Margus Veanes
FATES 2005 | July 2005
Exploration with Multiple State Groupings
Colin Campbell, Margus Veanes
Abstract State Machines 2005 | January 2005
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
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
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
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
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
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
Generating finite state machines from abstract state machines
Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Margus Veanes
ISSTA 2002 | July 2002
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
High-level Executable Specification of the Universal Plug and Play Architecture
Uwe Glässer, Yuri Gurevich, Margus Veanes
HICSS 2002 | January 2002
-
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.
People
Margus Veanes
Principal Researcher
Tony Hoare
Emeritus Researcher