Cartesian Hoare Logic for Verifying k-Safety Properties

Sousa, M., & Dillig, I. (2016). Cartesian Hoare Logic for Verifying k-Safety Properties. Proceedings of PLDI 2016, 57-69.

Type

Conference paper

Intellectual base

Primary research

Year

2016

DOI

10.1145/2908080.2908092

Link

https://doi.org/10.1145/2908080.2908092

Cited by

1 citation across 1 artifact.

Domain-specific

• Hyperproperty
  • k-safety. Many two-run security policies become ordinary safety properties of a product program, while higher-arity algebraic properties may require more traces.

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Registry ID ref:e6fc1beaf93a · see in the full table