Model Checking Real Time Java Using Java PathFinder. - Gary Lindstrom; Peter C. Mehlitz; Willem Visser (ATVA, 2005)

Design for Verification with Dynamic Assertions. - Peter C. Mehlitz; John Penix (SEW, 2005)

Model Checking Programs with Java PathFinder. - Willem Visser; Peter C. Mehlitz (SPIN, 2005)

Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. - Corina S. Pasareanu; Peter C. Mehlitz; David H. Bushnell; Karen Gundy-Burlet; Michael R. Lowry; Suzette Person; Mark Pape (ISSTA, 2008)

JPF-AWT: Model checking GUI applications. - Peter C. Mehlitz; Oksana Tkachuk; Mateusz Ujma (ASE, 2011)

X10X: Model Checking a New Programming Language with an "Old" Model Checker. - Milos Gligoric 001; Peter C. Mehlitz; Darko Marinov (ICST, 2012)

Modeling class loaders in Java PathFinder version 7. - Nastaran Shafiei; Peter C. Mehlitz (ACM SIGSOFT Softw. Eng. Notes, 2012)

A hands-on Java PathFinder tutorial. - Peter C. Mehlitz; Neha Rungta; Willem Visser (ICSE, 2013)

Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. - Corina S. Pasareanu; Willem Visser; David H. Bushnell; Jaco Geldenhuys; Peter C. Mehlitz; Neha Rungta (Autom. Softw. Eng., 2013)

Extending JPF to verify distributed systems. - Nastaran Shafiei; Peter C. Mehlitz (ACM SIGSOFT Softw. Eng. Notes, 2014)

Actor-Based Runtime Verification with MESA. - Nastaran Shafiei; Klaus Havelund; Peter C. Mehlitz (RV, 2020)

Concurrent runtime verification of data rich events. - Nastaran Shafiei; Klaus Havelund; Peter C. Mehlitz (Int. J. Softw. Tools Technol. Transf., 2023)

Smoke or cloud: Real-time satellite image segmentation in a wildfire data integration application. - Sequoia R. Andrade; Nastaran Shafiei; Peter C. Mehlitz (Comput. Geosci., 2025)