I describe an automated reasoning method which approaches programs in a way inspired by the way that a scientist approaches the natural world. The method uses iterated Abductive, Inductive and Deductive inference. It allows us to synthesize a pre/- post spec for a program procedure, without requiring any information about the procedure’s calling context. The method can be used to obtain partial specifications for portions of large code bases in the millions of lines of code. This talk presents a survey and further development of work with Cristiano Calcagno, Dino Distefano and Hongseok Yang, which aims to leverage ideas from Separation Logic in program analysis. Among other things, the method attempts to automate the discovery of assertions describing footprints (the resources that a program component accesses), in a bid to obtain modular analyses.