Back to Search
Start Over
MMC: the Mono Model Checker
- Source :
- Proceedings of the Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2007): 31 March 2007 • Braga, Portugal, 149-160, STARTPAGE=149;ENDPAGE=160;TITLE=Proceedings of the Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2007)
- Publication Year :
- 2007
- Publisher :
- Elsevier, 2007.
-
Abstract
- The Mono Model Checker (mmc) is a software model checker for cil bytecode programs. mmc has been developed on the Mono platform. mmc is able to detect deadlocks and assertion violations in cil programs. The design of mmc is inspired by the Java PathFinder (jpf), a model checker for Java programs. The performance of mmc is comparable to jpf. This paper introduces mmc and presents its main architectural characteristics.
- Subjects :
- Model checking
General Computer Science
Java
Programming language
Computer science
Assertion
software model checking
computer.software_genre
FMT-MC: MODEL CHECKING
n/a OA procedure
Theoretical Computer Science
Net
Bytecode
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Java pathfinder
Operating system
Mono
verification
cli bytecode
computer
mmc
Computer Science(all)
computer.programming_language
Subjects
Details
- Language :
- English
- Database :
- OpenAIRE
- Journal :
- Proceedings of the Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2007): 31 March 2007 • Braga, Portugal, 149-160, STARTPAGE=149;ENDPAGE=160;TITLE=Proceedings of the Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2007)
- Accession number :
- edsair.doi.dedup.....5e4b55eac3387754fe58b7aace5de772