Featherweight VeriFast

DOI10.2168/LMCS-11(3:19)2015zbMath1448.68221arXiv1507.07697MaRDI QIDQ3196351

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

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

separation logicprogram verificationsymbolic execution

Mathematics Subject Classification ID

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

Related Items (3)

A matching logic foundation for Alk ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Linear capabilities for fully abstract compilation of separation-logic-verified code

Uses Software

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

This page was built for publication: Featherweight VeriFast