Professor Zohar Manna (1939-2018), It pioneered the logical analysis of programs for correctness vis-à-specifications and for termination properties