Directed model checking is a bug-finding technique that emerged in the late 1990s, primarily applied to finite-state systems and infinite-state systems with finite quotient graphs such as timed automata. Recent progress in the areas of optimisation modulo theories and arithmetic abstractions of infinite-state systems makes it possible to apply this technique to efficiently (semi-)deciding reachability in inherently infinite-state systems that may even have undecidable reachability problems. In this talk, I will give an introduction to the ideas underlying directed model checking and demonstrate how it can be used to semi-decide reachability problems in large-scale Petri nets. This talk is based on joint work with M. Blondin and Ph. Offtermatt (Sherbrooke, CA)