On-the-Fly Techniques for Game-Based Software Model Checking

Adam Bakewell; Dan Ghica

doi:10.1007/978-3-540-78800-3_7

On-the-Fly Techniques for Game-Based Software Model Checking

Adam Bakewell, Dan Ghica

Computer Science

Research output: Contribution to journal › Article

10 Citations (Scopus)

Abstract

We introduce on-the-fly composition, symbolic modelling and lazy iterated approximation refinement for game-semantic models. We present Mage, an experimental model checker implementing this new technology. We discuss several typical examples and compare Mage with Blast and GameChecker, which are the state-of-the-art tools in on-the-fly software model checking, and game-based model checking.

Original language	English
Pages (from-to)	78-92
Number of pages	15
Journal	Lecture Notes in Computer Science
Volume	4963
DOIs	https://doi.org/10.1007/978-3-540-78800-3_7
Publication status	Published - 1 Jan 2008
Event	14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008) - Budapest, Hungary Duration: 29 Mar 2008 → 6 Apr 2008

Access to Document

10.1007/978-3-540-78800-3_7

Modular Abstraction and Abstraction Refinement: A Game Semantic Approach
Ghica, D.
Engineering & Physical Science Research Council
1/03/06 → 30/11/08
Project: Research Councils

Cite this

@article{9605c4283142483a9664fe801ed5eaf0,

title = "On-the-Fly Techniques for Game-Based Software Model Checking",

abstract = "We introduce on-the-fly composition, symbolic modelling and lazy iterated approximation refinement for game-semantic models. We present Mage, an experimental model checker implementing this new technology. We discuss several typical examples and compare Mage with Blast and GameChecker, which are the state-of-the-art tools in on-the-fly software model checking, and game-based model checking.",

author = "Adam Bakewell and Dan Ghica",

year = "2008",

month = jan,

day = "1",

doi = "10.1007/978-3-540-78800-3_7",

language = "English",

volume = "4963",

pages = "78--92",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer",

note = "14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008) ; Conference date: 29-03-2008 Through 06-04-2008",

}

TY - JOUR

T1 - On-the-Fly Techniques for Game-Based Software Model Checking

AU - Bakewell, Adam

AU - Ghica, Dan

PY - 2008/1/1

Y1 - 2008/1/1

N2 - We introduce on-the-fly composition, symbolic modelling and lazy iterated approximation refinement for game-semantic models. We present Mage, an experimental model checker implementing this new technology. We discuss several typical examples and compare Mage with Blast and GameChecker, which are the state-of-the-art tools in on-the-fly software model checking, and game-based model checking.

AB - We introduce on-the-fly composition, symbolic modelling and lazy iterated approximation refinement for game-semantic models. We present Mage, an experimental model checker implementing this new technology. We discuss several typical examples and compare Mage with Blast and GameChecker, which are the state-of-the-art tools in on-the-fly software model checking, and game-based model checking.

U2 - 10.1007/978-3-540-78800-3_7

DO - 10.1007/978-3-540-78800-3_7

M3 - Article

SN - 0302-9743

VL - 4963

SP - 78

EP - 92

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008)

Y2 - 29 March 2008 through 6 April 2008

ER -

On-the-Fly Techniques for Game-Based Software Model Checking

Abstract

Access to Document

Fingerprint

Projects

Modular Abstraction and Abstraction Refinement: A Game Semantic Approach

Cite this