The paper discusses the shift in focus of the formal methods community from special languages to analyzing programs written in modern programming languages. It presents Java PathFinder (JPF), a verification and testing environment for Java that integrates model checking, program analysis, and testing. JPF uses state compression, partial order and symmetry reduction, slicing, abstraction, and runtime analysis to reduce the state space. It has been applied to a real-time avionics operating system and a spacecraft controller model, illustrating the combination of abstraction, runtime analysis, and slicing with model checking. The paper argues that analyzing real programs can lead to new research directions and that formal methods should focus on real programs rather than designs. It also discusses the challenges of model checking Java programs, including the complexity of language constructs, the need to handle large state spaces, and the use of symmetry reductions, abstraction, static analysis, and runtime analysis to reduce the state space. JPF is described as a modular and understandable tool that can handle Java programs and has been used to analyze complex systems. The paper concludes that formal methods should focus on real programs and that JPF is a promising tool for this purpose.The paper discusses the shift in focus of the formal methods community from special languages to analyzing programs written in modern programming languages. It presents Java PathFinder (JPF), a verification and testing environment for Java that integrates model checking, program analysis, and testing. JPF uses state compression, partial order and symmetry reduction, slicing, abstraction, and runtime analysis to reduce the state space. It has been applied to a real-time avionics operating system and a spacecraft controller model, illustrating the combination of abstraction, runtime analysis, and slicing with model checking. The paper argues that analyzing real programs can lead to new research directions and that formal methods should focus on real programs rather than designs. It also discusses the challenges of model checking Java programs, including the complexity of language constructs, the need to handle large state spaces, and the use of symmetry reductions, abstraction, static analysis, and runtime analysis to reduce the state space. JPF is described as a modular and understandable tool that can handle Java programs and has been used to analyze complex systems. The paper concludes that formal methods should focus on real programs and that JPF is a promising tool for this purpose.