Cartesian hoare logic for verifying k-safety properties
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jun 02, 2016
- Source ID
- 10.1145/2980983.2908092
Entities
People
- Işıl Dillig
- Marcelo C. Sousa
Organizations
- Air Force Research Laboratory
- National Science Foundation
- University of Oxford
- University of Texas at Austin