Featherweight VeriFast

DOI10.2168/LMCS-11(3:19)2015MaRDI QIDQ3196351zbMATH OpenFDO

Authors Bart Jacobs, Frédéric Vogels, Frank Piessens

Publication date 29 October 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.07697

zbMATH Keywords

program verificationseparation logicsymbolic execution

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: VeriFast is a leading research prototype tool for the sound modular verification of safety and correctness properties of single-threaded and multithreaded C and Java programs. It has been used as a vehicle for exploration and validation of novel program verification techniques and for industrial case studies; it has served well at a number of program verification competitions; and it has been used for teaching by multiple teachers independent of the authors. However, until now, while VeriFast's operation has been described informally in a number of publications, and specific verification techniques have been formalized, a clear and precise exposition of how VeriFast works has not yet appeared. In this article we present for the first time a formal definition and soundness proof of a core subset of the VeriFast program verification approach. The exposition aims to be both accessible and rigorous: the text is based on lecture notes for a graduate course on program verification, and it is backed by an executable machine-readable definition and machine-checked soundness proof in Coq.

Recommendations

• Computer Aided Verification
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Dafny: an automatic program verifier for functional correctness
• scientific article; zbMATH DE number 1982210
• Verification of concurrent systems with VerCors

Cited in

(8)

• TRACER: a symbolic execution tool for verification
• Mostly sound type system improves a foundational program verifier
• Dafny: an automatic program verifier for functional correctness
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• A matching logic foundation for Alk
• An algebraic glimpse at bunched implications and separation logic
• Controlling unfolding in type theory
• A mechanized first-order theory of algebraic data types with pattern matching

Describes a project that uses

Uses Software

• Coq
• VCC
• VeriFast
• Toolchain
• SLAyer
• HIP
• Smallfoot
• VeriSmall
• jStar
• seL4
• Infer
• Charge!

This page was built for publication: Featherweight VeriFast

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196351)