We study automated techniques to verify the reliability, security, and safety of complex software, including cyber-physical systems and artificial intelligence systems.