Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays
No abstract available.
Related papers
- SecCSL: Security Concurrent Separation Logic CAV 2019
- ConCert: a smart contract certification framework in Coq CPP 2020
- Higher order symbolic execution for contract verification and refutation JFP 2017
- Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication TACAS 2016
- Towards Complete Reasoning about Axiomatic Specifications VMCAI 2011
- Invariant Synthesis for Incomplete Verification Engines TACAS 2018
- Rich specifications for Ethereum smart contract verification OOPSLA 2021
- Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification VMCAI 2026