Cartesian hoare logic for verifying k-safety properties
2016pp. 57–69
Citations Over TimeTop 1% of 2016 papers
Abstract
Unlike safety properties which require the absence of a “bad” program trace, k-safety properties stipulate the absence of a “bad” interaction between k traces. Examples of k-safety properties include transitivity, associativity, anti-symmetry, and monotonicity. This paper presents a sound and relatively complete calculus, called Cartesian Hoare Logic (CHL), for verifying k-safety properties. We also present an automated verification algorithm based on CHL and implement it in a tool called DESCARTES. We use DESCARTES to analyze user-defined relational operators in Java and demonstrate that DESCARTES is effective at verifying (or finding violations of) multiple k-safety properties.
Related Papers
- → Certified assembly programming with embedded code pointers(2006)112 cited
- → Compiler verification meets cross-language linking via data abstraction(2014)31 cited
- → Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics(2007)19 cited
- Provably correct graph transformations with small-tALC(2015)
- → DETERMINING QUALITY REQUIREMENTS AT THE UNIVERSITIES TO IMPROVE THE QUALITY OF EDUCATION(2018)