Predicate abstraction for hyperliveness verification

DOI10.1007/S10703-025-00482-5MaRDI QIDQ6938564zbMATH OpenFDO

Authors Raven Beutner, Bernd Finkbeiner

Publication date 25 August 2025

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

verificationinfinite-state systemssoftware verificationpredicate abstractionhyperpropertieshyperLTLprogram reductionhyperliveness

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 7730626 (Why is no real title available?)
• A constraint-based approach to solving games on infinite graphs
• A temporal logic for asynchronous hyperproperties
• Algorithms for model checking HyperLTL and HyperCTL^*
• Alignment completeness for relational Hoare logics
• Asynchronous extensions of hyperLTL
• AutoHyper: explicit-state model checking for HyperLTL
• Automated hypersafety verification
• Beyond 2-safety: asymmetric product programs for relational program verification
• Bounded model checking for hyperproperties
• Causality-based game solving
• Computer Aided Verification
• Constraint-based relational verification
• Deciding hyperproperties combined with functional specifications
• Defining liveness
• Expressiveness and decidability of temporal logics for asynchronous hyperproperties
• Formal certification of code-based cryptographic proofs
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Hypernode automata
• Is Your Software on Dope?
• Lazy abstraction
• Model-Checking HyperLTL for Pushdown Systems
• Permissive strategies: from parity games to safety games
• Predicate Abstraction with Under-approximation Refinement
• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• Predicate abstraction for program verification
• Property directed self composition
• RHLE: modular deductive verification of relational \(\forall \exists\) properties
• Reduction
• Refinement of Trace Abstraction
• Second-order hyperproperties
• Secure information flow by self-composition
• Simple relational correctness proofs for static analyses and program transformations
• Software Verification of Hyperproperties Beyond k-Safety
• Solving Games Via Three-Valued Abstraction Refinement
• The existence of refinement mappings
• The power of symbolic automata and transducers
• Unifying hyper and epistemic temporal logics
• Verifying hyperliveness

This page was built for publication: Predicate abstraction for hyperliveness verification

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