Logics for correctness aim to prove error absence but rely on over-approximations, leading to false alarms that can hamper programmer productivity. Conversely, logics for incorrectness expose true bugs by using under-approximations. We combine forward and backward reasoning for incorrectness: first, a forward analysis using O’Hearn’s Incorrectness Logic (IL) identifies some reachable errors. Then, a backward analysis, led by a new variant of Ascari et al.’s Sufficient Incorrectness Logic (SIL) and guided by IL’s proof tree, reveals the preconditions responsible for errors. Beyond theoretical and practical advances that our proof system can enact for program analysis, we highlight its novel logical judgement format, called UT format (for u-turn), here exemplified for forward-driven backward analysis: we argue that it can be readily adapted to other settings, e.g., to use the SIL proofs to guide the IL inference of reachable errors.