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

Research output: Contribution to journalArticle

Colleges, School and Institutes


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 languageEnglish
Pages (from-to)78-92
Number of pages15
JournalLecture Notes in Computer Science
Publication statusPublished - 1 Jan 2008
Event14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008) - Budapest, Hungary
Duration: 29 Mar 20086 Apr 2008