#306: [Provable Security Podcast Series Episode #1]: Automated Reasonings Past, Present, and Future with Moshe Vardi

Published: April 3, 2019, 8:34 p.m.

b'Provable Security: Conversations on Next Gen Security. We published a podcast (https://aws.amazon.com/podcasts/aws-podcast/#266) on provable security (https://aws.amazon.com/security/provable-security/) last fall, and, due to high customer interest, we decided to bring you a regular peek into this AWS initiative. This series will cover how the traditionally academic field of automated reasoning is being applied at AWS at scale to help provide higher assurances for our customers, regulators, and the broader cloud industry. We\\u2019ll talk to individuals whose minds helped shape the history of automated reasoning, as well as learn from engineers and scientists who are applying automated reasoning to help solve pressing security and privacy challenges in the cloud.\\n \\nIn our first interview, Byron Cook, Director of the AWS Automated Reasoning Group, sits down with Moshe Vardi, Karen Ostrum George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology. Moshe describes the history of logic, automated reasoning, formal verification and his legendary moustache.\\n \\nLearn more at the AWS Provable Security webpage (https://aws.amazon.com/security/provable-security/).\\nAutomated reasoning public figures:\\n\\nGeorge Boole https://en.wikipedia.org/wiki/George_Boole\\nTony Hoare https://en.wikipedia.org/wiki/Tony_Hoare\\nRobert W. Floyd https://en.wikipedia.org/wiki/Robert_W._Floyd\\nJohn McCarthy https://en.wikipedia.org/wiki/John_McCarthy_(computer_scientist)\\nAmir Pnueli https://en.wikipedia.org/wiki/Amir_Pnueli\\nGottlob Frege https://en.wikipedia.org/wiki/Gottlob_Frege\\nArthur Prior https://en.wikipedia.org/wiki/Arthur_Prior\\nJohn Harrison https://www.cl.cam.ac.uk/~jrh13/\\n\\nAutomated techniques and algorithms:\\n\\nFirst-order logic https://en.wikipedia.org/wiki/First-order_logic\\nTemporal logic https://en.wikipedia.org/wiki/Temporal_logic\\nAn Automata-Theoretic Approach to Automatic Program Verification https://orbi.uliege.be/bitstream/2268/116609/1/lics86.pdf\\nBoolean satisfiability problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem\\nDavis-Putnam algorithm https://en.wikipedia.org/wiki/Davis\\u2013Putnam_algorithm\\nSAT Competition https://www.satcompetition.org/'