Sciweavers

Share
TAICPART
2006
IEEE

Bogor: A Flexible Framework for Creating Software Model Checkers

8 years 9 months ago
Bogor: A Flexible Framework for Creating Software Model Checkers
Model checking has proven to be an effective technology for verification and debugging in hardware and more recently in software domains. With the proliferation of multicore architectures and a greater emphasis on distributed computing, model checking is an increasingly important software quality assurance technique that can complement existing testing and inspection methods. We believe that recent trends in both the requirements for software systems and the processes by which systems are developed suggests 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 article, we summarize how Bogor provides direct support for modeling object-oriented designs and implementations, how its modeling language and algorithms can be extended and customized to ...
Robby, Matthew B. Dwyer, John Hatcliff
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where TAICPART
Authors Robby, Matthew B. Dwyer, John Hatcliff
Comments (0)
books