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

DOI10.1007/978-3-662-46669-8_7zbMATH Open1335.68063OpenAlexW905467040MaRDI QIDQ2802435FDOQ2802435

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

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

Mathematics Subject Classification ID

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

Cited In (2)

• Characteristic formulae for liveness properties of non-terminating CakeML programs
• Connecting Higher-Order Separation Logic to a First-Order Outside World

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)