Abstract

This chapter presents how to prove ACSL properties of C programs with the Wp plug-in of Frama-C using deductive verification and SMT solvers or Proof Assistants. Specifically, this chapter explores the internals of the Wp plug-in, with a specific focus on how ACSL and C are encoded into classical first-order logic, including its various memory models. Then, the internal proof strategy of Wp is described, which leads to a discussion on specification methodology and proof engineering, and how to interact with the Wp plug-in. Finally, we compare Wp with a selection of other amazing systems and logics for the deductive verification of C programs.

In

Guide to Software Verification with Frama-C. ISBN 978-3-031-55608-1

DOI: 10.1007/978-3-031-55608-1_4