# RHLE: Automatic Verification of $\forall\exists$-Hyperproperties

@article{Dickerson2020RHLEAV, title={RHLE: Automatic Verification of \$\forall\exists\$-Hyperproperties}, author={Robert Dickerson and Qianchuan Ye and Benjamin Delaware}, journal={arXiv: Programming Languages}, year={2020} }

Specifications of program behavior typically consider single executions of a program, usually requiring that every execution never reaches a bad state (a safety property) or that every execution can eventually produce some good state (a liveness property). Many desirable behaviors, however, including refinement and non-interference, range over multiple executions of a program. These sorts of behaviors are instead expressible as a combination of k-safety and k-liveness hyperproperties… Expand

#### References

SHOWING 1-10 OF 22 REFERENCES

Verifying Hyperliveness

- Computer Science
- CAV
- 2019

This paper reduces existential quantification to strategic choice and shows that synthesis algorithms can be used to eliminate the existential quantifiers automatically and can be extended to reactive system synthesis, i.e., to automatically construct a reactive system that is guaranteed to satisfy a given HyperLTL formula. Expand

Cartesian hoare logic for verifying k-safety properties

- Computer Science
- PLDI 2016
- 2016

This paper presents a sound and relatively complete calculus, called Cartesian Hoare Logic (CHL), for verifying k-safety properties, and presents an automated verification algorithm based on CHL and implement it in a tool called DESCARTES. Expand

Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification

- Computer Science
- LFCS
- 2013

Relational Hoare Logic is a generalization of Hoare logic that allows reasoning about executions of two programs, or two executions of the same program. It can be used to verify that a program is… Expand

Semantical consideration on floyo-hoare logic

- Computer Science
- 17th Annual Symposium on Foundations of Computer Science (sfcs 1976)
- 1976

An appropriate axiom system is given which is complete for loop-free programs and also puts conventional predicate calculus in a different light by lumping quantifiers with non-logical assignments rather than treating them as logical concepts. Expand

Temporal Logics for Hyperproperties

- Computer Science, Mathematics
- POST
- 2014

It is shown that the quantification over paths naturally subsumes other extensions of temporal Logic with operators for information flow and knowledge, and the model checking problem for temporal logic with path quantification is decidable. Expand

Maximal specification synthesis

- Computer Science
- POPL 2016
- 2016

A novel approach is presented that utilizes a counterexample-guided inductive synthesis loop and reduces the maximal specification inference problem to multi-abduction, and the novel notion of multi- abduction as a generalization of classical logical abduction is formulated. Expand

Relational abstract interpretation for the verification of 2-hypersafety properties

- Computer Science
- CCS
- 2013

A framework for proving 2-hypersafety properties by means of abstract interpretation on the self-compositions of the control flow graphs of programs to prove intricate information flow properties of programs written in a simple language for tree manipulation motivated by the Web Services Business Process Execution Language. Expand

Verification Tools for Finite-State Concurrent Systems

- Computer Science
- REX School/Symposium
- 1993

This paper describes in detail how the new implementation works and gives realistic examples to illustrate its power, and discusses a number of directions for future research. Expand

Simple relational correctness proofs for static analyses and program transformations

- Computer Science
- POPL '04
- 2004

We show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and proved correct using elementary logical and… Expand

Relational Verification Using Product Programs

- Computer Science
- FM
- 2011

This work provides a general notion of product program that supports a direct reduction of relational verification to standard verification, and illustrates the benefits of the method with selected examples, including non-interference, standard loop optimizations, and a state-of-the-art optimization for incremental computation. Expand