Skip to main navigation Skip to search Skip to main content

Model-checking multi-threaded distributed Java programs

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

64 Scopus citations

Abstract

Systematic state-space exploration is a powerful technique for verification of concurrent software systems. Most work in this area deals with manually-constructed models of those systems. We propose a framework for applying state-space exploration to multi-threaded distributed systems written in standard programming languages. It generalizes Godefroid’s work on VeriSoft, which does not handle multi-threaded systems, and Bruening’s work on ExitBlockRW, which does not handle distributed (multi-process) systems. Unlike ExitBlockRW, our search algorithms incorporate powerful partial-order methods, guarantee detection of deadlocks, and guarantee detection of violations of the locking discipline used to avoid race conditions in accesses to shared variables.

Original languageEnglish
Title of host publicationSPIN Model Checking and Software Verification - 7th International SPIN Workshop, Proceedings
EditorsKlaus Havelund, John Penix, Willem Visser
PublisherSpringer Verlag
Pages224-244
Number of pages21
ISBN (Print)3540410309, 9783540410300
DOIs
StatePublished - 2000
Event7th International SPIN Workshop on Model Checking and Software Verification, 2000 - Stanford, United States
Duration: Aug 30 2000Sep 1 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1885
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International SPIN Workshop on Model Checking and Software Verification, 2000
Country/TerritoryUnited States
CityStanford
Period08/30/0009/1/00

Fingerprint

Dive into the research topics of 'Model-checking multi-threaded distributed Java programs'. Together they form a unique fingerprint.

Cite this