Formal Verification of Programs containing Inline Assembly

Speaker: Gurvan Debaussart <u>EDIC candidacy exam</u><br> Exam president: Prof. Clément Pit-Claudel<br> Thesis advisor: Prof. Thomas Bourgeat<br> Co-examiner: Prof. Nate Foster<br> <br> <u>Abstract</u><br> <br> <u>Selected papers</u><br> - Formal requirements for virtualizable third generation architectures (<a href="https://dl.acm.org/doi/10.1145/361011.361073">https://dl.acm.org/doi/10.1145/361011.361073</a>)<br> - Get Rid of Inline Assembly Through Verification Oriented Lifting (<a href="https://cea.hal.science/cea-04228170/file/long_paper.pdf">https://cea.hal.science/cea-04228170/file/long_paper.pdf</a>)<br