Sound, modular and compositional verification of the input/output behavior of programs

DOI10.1007/978-3-662-46669-8_7MaRDI QIDQ2802435zbMATH OpenOpenAlexFDO

Authors Willem Penninckx, Frank Piessens, Bart Jacobs

Publication date 26 April 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://lirias.kuleuven.be/handle/123456789/478356

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Program verification: state of the art, problems, and results. I
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Compositional verification of sequential programs with procedures
• Modular verification of programs with effects and effects handlers
• scientific article; zbMATH DE number 176727

Cited in

(2)

• Connecting higher-order separation logic to a first-order outside world
• Characteristic formulae for liveness properties of non-terminating CakeML programs

Describes a project that uses

Uses Software

• VeriFast
• Ynot

This page was built for publication: Sound, modular and compositional verification of the input/output behavior of programs

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