Formal bytes: The Axiomise Podcast Channel

In the 50th episode of our podcast, Dr Darbari talks to Dr Amin Shokrollahi. We trace Amin's journey from his early childhood, his interests in Mathematics to his current position as a CEO of Kandou - a company that specialises in low-power, high-speed, off-chip communication solutions. Amin describes himself as more of a mathematician than an electronics engineer. He outlines how he uses principles of abstraction in Mathematics/CS in real-life projects. Amin explains the retimer technology that Kando uses in their cutting-edge Matterhorn USB Type-C solution.

How can we make teaching formal methods more effective? What is the relationship between SQL and first-order logic? We used logic to design computers, now we use computers to perform logic reasoning, so is there a relation between machine learning and logic? How does a human brain perform reasoning? Is machine learning and logic the answer to all the major questions facing society? How do incomplete information and statistical bias fit into this? What does risk assessment mean? Tune in to our latest podcast to hear what Prof. Vardi has to say about these topics.

This week Dr Darbari talks to Prof. Moshe Vardi - one of the best-known names in computing and formal methods. In the first of the two episodes, we trace Moshe's journey from his early years and talk about logic, applications of logic to law, NP-complete problems, ENIAC, John von Neumann, John Backus, compilers, semantics, abstractions, descriptions. Moshe shares fascinating accounts of chat with Ed Clarke and the history of LTL, CTL, SVA and PSL. Find out why model checking works. Thank you very much, Moshe, for taking time out to talk to us.

Pleased to bring up the second part of the chat with Prof. Supratik Chakaraborty from IIT Bombay. We talk on boolean function synthesis, AI/ML, BDDs and SAT. Find out the next big thing in synthesis that has the potential to break the RSA! 

Prof. Supratik Chakraborty is our guest this week. Tune in to find out how he came full circle from the corridors of IIT in his under-grad to being one of the top leaders in formal methods at IIT Bombay. In the first of the two-part podcast, Supratik talks to Dr Darbari about his passion for asynchronous circuits & formal methods, and word-level abstractions, and symbolic trajectory evaluation. Supratik shares his insights in teaching and research in formal methods and makes a strong case about why formal methods would be necessary for the design of machine learning hardware.

This week Dr Darbari talks to Ravi Thummarukudy. Hear Ravi's fascinating story from growing up in a village in Kerala with no electricity to being a CEO of one of the top design IP companies Mobiveil Inc. From IIT Madras, and days at ISRO, Ravi describes how he moved on to make Mobiveil a trustworthy name in design IP using the mantra trust but verify.

This week we discuss our new formal verification course launched on 6 April, last week. If you're looking to understand how to apply formal methods, especially for industrial projects in VLSI, then we have something for you.

This week, Dr. Darbari talks to Dr. Daniel Zimmerman, Principal Researcher from Galois Inc. Lot of exciting conversation on formal methods and their applications to cryptography, homomorphic computing and Daniel also reveals the secret Ninja formal methods and the work done with Amazon on deploying software analysis.

This week Bob Smith is our guest. Bob is an executive director of the ESD Alliance, a SEMI Strategic Association Partner. He is responsible for the management and operations of the ESD Alliance, an international association of companies providing goods and services throughout the semiconductor design ecosystem.

How do we know when the proof is the valid proof? Can we always see the proof? Are visible proofs required for verification? Can you trust invisible proofs for sign-off? Welcome to formal verification! Tune in to this week's podcast to learn more.