[cs-talks] Upcoming CS Seminars: Seminar in Formal Verification and High-Assurance Software (Wed)

Greenwald, Faith fgreen1 at bu.edu
Mon Jan 11 11:57:43 EST 2016


Verification of Programs Using Frama-C and Why3

Aleksy Schubert, University of Warsaw
Wednesday, January 13, 2016 at 2pm in MCS 148

Abstract: Frama-C is a tool that makes it possible to do a variety of analyses for C programs annotated with C specification language called ACSL (The ANSI/ISO C Specification Langage). One of the possible ways to use Frama-C is to generate verification conditions for appropriately defined Hoare logic that is in line with C programming language semantics. These verification conditions can subsequently be discharged by Why3 tool together with a number of proving engines such as Alt-Ergo, CVC4, Z3, Coq etc. that makes it possible to manage the proving of necessary properties. During the talk I will present an overview of the tools and show a number of interesting examples to demonstrate how these tools work together to make possible verification of practical programs.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs-mailman.bu.edu/pipermail/cs-talks/attachments/20160111/cbf7ca56/attachment.html>


More information about the cs-talks mailing list