How to make concurrent programs highly reliable-more than state space analysis

Several approaches to making concurrent programs highly reliable are surveyed. State space analysis including model checking is the most promising formal verification approach for concurrent programs. However, it is not the only such method for actual program development. The paper focuses on harmful nondeterministic behaviors of concurrent programs and introduces three advanced approaches (testing with verification, program adjustment, and hypersequential programming) to detect and remove them, which provide more than state space analysis. We also show our projects and tools going along with these approaches