University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Verasco, a formally verified C static analyzer

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Verasco, a formally verified C static analyzer

Download to your calendar using vCal

If you have a question about this talk, please contact .

Please be aware that this event may be recorded. Microsoft will own the copyright of any recording and reserves the right to distribute it as required.

This talk will present the design and soundness proof of Verasco, a formally verified static analyzer for most of the ISO C99 language (excluding recursion and dynamic allocation), developed using the Coq proof assistant. Verasco aims at establishing the absence of run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. It include a memory abstract domain, an abstract domain of arithmetical symbolic equalities, an abstract domain of intervals, an abstract domain of arithmetical congruences and an octagonal abstract domain. Verasco integrates with the CompCert formally-verified C compiler so that not only the soundness of the analysis results is guaranteed with mathematical certitude, but also the fact that these guarantees carry over to the compiled code.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

City House, Hills Road, Cambridge CB2 1RY Lecture Theatre, Level 7, www.mrc-dunn.cam.ac.uk In person in the Max Perutz Lecture Theatre (CB2 0QH) and via Zoom, link: https://mrc-lmb-cam-ac-uk.zoom.us/j/92958233734?pwd=eDI1dkNlTFNQc2lxUVV4S2JHRlFmZz09

Other talks

Machine Learning for Spectral Geometry and Vice Versa How bubble acoustics can help in three apocalypses Title to be confirmed Feedback and the circumgalactic medium Ice in a mostly-Arctic Context TBC
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity