Described is a system for automatically generating images that satisfy specific image properties. Using a code parser component, a tensor expression intermediate representation (IR) of a deep neural network code is produced. A specification describing a set of image properties is parsed in a fixed formal syntax. The tensor expression IR and the specification is input into a rewriting and analysis engine. The rewriting and analysis engine queries an external solver to obtain pixel values satisfying the specification. When pixel values satisfying the specification can be found in a fixed time period, the rewriting and analysis engine combines the pixel values into an image that satisfies the specification and outputs the image.