Byron Cook: Neurosymbolic AI at Amazon Web Services

From November 10 to 11, Professor Byron Cook visited the FORSYTE Research Unit at TU Wien Informatics, where he held a lecture describing recent advancements of Neurosymbolic AI at Amazon Web Services (AWS). The talk was held as part of the regular lecture series for the master’s courses Formal Methods in Systems Engineering and Automated Deduction at TU Wien. Byron Cook is a vice president and distinguished scientist at Amazon, program manager at the Defense Advanced Research Projects Agency (DARPA), and a professor at the University College London (UCL). He is well-known for his work on automatic methods for proving program termination and the Terminator termination prover, showcasing that automatic termination proving was impossible. He contributed to Microsoft’s SLAM and Static Driver Verifier. Bryan Cook revived automatic program verification research in various ways and founded Amazon’s Automated Reasoning Group (ARG). He has received multiple awards for his research contributions, notably the Roger Needham Award and the distinction of Fellow of the Royal Academy of Engineering.