Sciweavers

Share
CAV
2005
Springer

Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework

10 years 1 months ago
Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework
Model checking has proven to be an effective technology for verification and debugging in hardware and more recently in software domains. We believe that recent trends in both the requirements for software systems and the processes by which systems are developed suggest that domain-specific model checking engines may be more effective than general purpose model checking tools. To overcome limitations of existing tools which tend to be monolithic and non-extensible, we have developed an extensible and customizable model checking framework called Bogor. In this tool paper, we summarize (a) Bogor’s direct support for modeling object-oriented designs and implementations, (b) its facilities for extending and customizing its modeling language and algorithms to create domain-specific model checking engines, and (c) pedagogical materials that we have developed to describe the construction of model checking tools built on top of the Bogor infrastructure. Motivation Temporal logic model c...
Matthew B. Dwyer, John Hatcliff, Matthew Hoosier,
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CAV
Authors Matthew B. Dwyer, John Hatcliff, Matthew Hoosier, Robby
Comments (0)
books