Property directed self composition

DOI10.1007/978-3-030-25540-4_9MaRDI QIDQ6194570zbMATH OpenOpenAlexFDO

Authors Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel

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.07705

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 address the problem of verifying k-safety properties: properties that refer to k-interacting executions of a program. A prominent way to verify k-safety properties is by self composition. In this approach, the problem of checking k-safety over the original program is reduced to checking an "ordinary" safety property over a program that executes k copies of the original program in some order. The way in which the copies are composed determines how complicated it is to verify the composed program. We view this composition as provided by a semantic self composition function that maps each state of the composed program to the copies that make a move. Since the "quality" of a self composition function is measured by the ability to verify the safety of the composed program, we formulate the problem of inferring a self composition function together with the inductive invariant needed to verify safety of the composed program, where both are restricted to a given language. We develop a property-directed inference algorithm that, given a set of predicates, infers composition-invariant pairs expressed by Boolean combinations of the given predicates, or determines that no such pair exists. We implemented our algorithm and demonstrate that it is able to find self compositions that are beyond reach of existing tools.

Recommendations

• Self-composition by symbolic execution
• Lazy self-composition for security verification
• Automated hypersafety verification
• Property-directed inference of universal invariants or proving their absence

Cited in

(10)

• Constraint-based relational verification
• Product programs in the wild: retrofitting program verifiers to check information flow security
• Software Verification of Hyperproperties Beyond k-Safety
• Automated hypersafety verification
• Compositional model checking for multi-properties
• Alignment complete relational Hoare logics for some and all
• Certified verification of relational properties
• Symbolic execution for refuting hyperproperties
• Lockstep composition for unbalanced loops
• Predicate abstraction for hyperliveness verification

This page was built for publication: Property directed self composition

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