Computer systems are increasingly coming to be relied upon to augment or replace human
operators in controlling mechanical devices in contexts such as transportation systems, chemical
plants, and medical devices, where safety and correctness are critical. A central problem is how
to verify that such partially automated or fully autonomous cyber-physical systems (CPS) are
worthy of our trust. One promising approach involves synthesis of the computer implementation
