Mechanizing Abstract Interpretation - Challenges and Applications
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore the challenges and successes of formalizing abstract interpretation theory using proof assistants in this 46-minute conference talk by Xavier Leroy. Delve into the motivations behind machine-assisted proofs for mathematical theories and formal verification of static analyzers. Examine multiple attempts to mechanize abstract interpretation using the Coq proof assistant, drawing from David Pichardie's PhD work and the Verasco verified static analyzer project. Compare these efforts with similar work by Nipkow and Darais and Van Horn using other proof assistants. Discover the strengths of proving soundness for static analyzers based on abstract interpretation, while also addressing the difficulties in formalizing certain aspects of classic abstract interpretation theory within Coq. Analyze whether these challenges stem from limitations specific to Coq or are inherent to other logical systems, gaining insights into the complexities of mechanizing abstract interpretation.
Syllabus
[N40AI'24] Mechanizing Abstract Interpretation
Taught by
ACM SIGPLAN
Related Courses
Secure Software Development: Verification and More Specialized TopicsLinux Foundation via edX Developing Secure Software
LinkedIn Learning Ethical Hacking: Mobile Devices and Platforms
LinkedIn Learning Tüm Aşamalarıyla İnşaat Eğitimi - AUTOCAD/STA4/EXCEL/PROJECT
Udemy Mobile Security: Reverse Engineer Android Apps From Scratch
Udemy