Automated hypersafety verification

DOI10.1007/978-3-030-25540-4_11arXiv1905.09242OpenAlexW2962297646MaRDI QIDQ6194574FDOQ6194574

Anthony Vandikas, Azadeh Farzan

Publication date: 16 February 2024

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

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.

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)

Cited In (6)

• Constraint-based relational verification
• Software Verification of Hyperproperties Beyond k-Safety
• Decomposing data structure commutativity proofs with \(mn\)-differencing
• A pragmatic approach to stateful partial order reduction
• Verification of concurrent programs using Petri net unfoldings
• Commutativity for concurrent program termination proofs

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)