Implementing Separation Logic Using an SMT-backed Frame Rule

Offered By: ACM SIGPLAN via YouTube

Course Description

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!

Explore a 22-minute conference talk from ACM SIGPLAN's WITS'24 that delves into implementing separation logic using an SMT-backed Frame Rule. Learn about the integration of symbolic execution and separation logic for program verification, focusing on the recent advancements in SMT solvers like CVC5. Discover how this implementation can simplify the machinery dealing with separation logic in tools such as Smallfoot and GRASShopper. Gain insights into the challenges and potential solutions for reasoning about code with pointers or references using SMT queries and the Frame Rule.

Syllabus

[WITS'24] Implementing separation logic using an SMT-backed Frame Rule

Taught by

ACM SIGPLAN

Related Courses

Reverse Engineering 3201: Symbolic Analysis
OpenSecurityTraining2 via Independent Logic Against Sneak Obfuscated Malware
NorthSec via YouTube SMT- Quantifiers, and Future Prospects - IPAM at UCLA
Institute for Pure & Applied Mathematics (IPAM) via YouTube SMT Solvers in IT Security - Deobfuscating Binary Code with Logic
Cooper via YouTube Jumping the Fence - Comparison and Improvements for Existing Jump Oriented Programming Tools
YouTube