Inquiry About Differences Between JPF and Other Model Checkers

[bupt01]

I am currently exploring Java Pathfinder (JPF) as a model checker and am fascinated by its ability to explore the entire state space of programs. However, I have also come across other model checking tools such as MCR[1] and CBMC[2], which serve different purposes—MCR being a stateless model checker and CBMC being a stateful model checker.

I would like to understand the key differences between JPF and these tools, particularly in terms of their approaches, capabilities, and use cases. Unfortunately, I have not found a clear comparison or discussion of this in the existing literature.

Could you please provide some insights or resources that clarify these distinctions?

Thank you very much for your assistance.

[1]Stateless Model Checking Concurrent Programs with Maximal Causality Reduction
[2]The C Bounded Model Checker: