Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays

DOI10.1007/978-3-642-11957-6_4zbMath1260.68048OpenAlexW1870297738MaRDI QIDQ3558215

John Hatcliff, Torben Amtoft, Edwin Rodríguez

Publication date: 4 May 2010

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

Full work available at URL: https://doi.org/10.1007/978-3-642-11957-6_4

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Relational Decomposition

Uses Software

• SPARK

This page was built for publication: Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays