The Thesis Review [43] Swarat Chaudhuri - Logics and Algorithms for Software Model Checking
Jun 28, 2022
Swarat Chaudhuri, an Associate Professor at the University of Texas, delves into the fascinating intersection of programming languages and machine learning. He discusses the evolution of formal verification and the integration of model checking within AI systems. The conversation highlights advancements in neurosymbolic programming, enhancing reliability in software. Swarat also provides insights on developing reusable modules and emphasizes the importance of practical contributions in research, especially in AI safety and real-world applications.
AI Snips
Chapters
Transcript
Episode notes
AI Internship
- Swarat Chaudhuri considered interning in neural networks.
- An advisor discouraged him, saying AI was a dead field.
Program Reasoning vs. AI Reasoning
- Reasoning about programs uses formal semantics, treating them as mathematical objects.
- AI reasoning often involves uncertainty, while program reasoning uses adversarial assumptions.
Model Checking
- Model checking uses search-based methods to find bugs or verify system correctness.
- It explores all possible states to ensure requirements are met.