Automated hypersafety verification

DOI10.1007/978-3-030-25540-4_11MaRDI QIDQ6194574zbMATH OpenOpenAlexFDO

Authors Azadeh Farzan, Anthony Vandikas

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1905.09242

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We propose an automated verification technique for hypersafety properties, which express sets of valid interrelations between multiple finite runs of a program. The key observation is that constructing a proof for a small representative set of the runs of the product program (i.e. the product of the several copies of the program by itself), called a reduction, is sufficient to formally prove the hypersafety property about the program. We propose an algorithm based on a counterexample-guided refinement loop that simultaneously searches for a reduction and a proof of the correctness for the reduction. We demonstrate that our tool Weaver is very effective in verifying a diverse array of hypersafety properties for a diverse class of input programs.

Recommendations

• Software Verification of Hyperproperties Beyond k-Safety
• Algorithms for model checking HyperLTL and HyperCTL^*
• AutoHyper: explicit-state model checking for HyperLTL
• Property directed self composition

Cited in

(12)

• Constraint-based relational verification
• Software Verification of Hyperproperties Beyond k-Safety
• Property directed self composition
• Decomposing data structure commutativity proofs with \(mn\)-differencing
• A pragmatic approach to stateful partial order reduction
• Alignment complete relational Hoare logics for some and all
• Choose your proofs: commutativity and symmetry for smarter reasoning
• Verification of concurrent programs using Petri net unfoldings
• Temporal hyperproperties for population protocols
• Symbolic execution for refuting hyperproperties
• Commutativity for concurrent program termination proofs
• Predicate abstraction for hyperliveness verification

This page was built for publication: Automated hypersafety verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6194574)