Formally Verifying that a Program Does What It Should: The Wp Plug-in

This chapter presents how to prove ACSL properties of C programs with the WpWp plug-in of Frama-C using deductive verification and SMT solvers or Proof Assistants. Specifically, this chapter explores the internals of the WpWp 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 WpWp is described, which leads to a discussion on specification methodology and proof engineering, and how to interact with the WpWp plug-in. Finally, we compare WpWp with a selection of other amazing systems and logics for the deductive verification of C programs.