Bounded model checking for asynchronous hyperproperties

DOI10.1007/978-3-031-30823-9_2MaRDI QIDQ6535338zbMATH OpenFDO

Authors Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner, César Sánchez

Publication date 13 December 2023

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30823-9_2

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A temporal logic for asynchronous hyperproperties
• Asynchronous extensions of hyperLTL
• Bounded model checking for hyperproperties
• Probabilistic Hyperproperties with Nondeterminism
• On verifying timed hyperproperties

Cites work

• A temporal logic for asynchronous hyperproperties
• Algorithms for model checking HyperLTL and HyperCTL^*
• Bounded model checking for hyperproperties
• Verifying hyperliveness
• Witnessing secure compilation

Cited in

(7)

• scientific article; zbMATH DE number 1629966 (Why is no real title available?)
• Exploiting step semantics for efficient bounded model checking of asynchronous systems
• Model checking quantitative hyperproperties
• Efficient loop conditions for bounded model checking hyperproperties
• Symbolic execution for refuting hyperproperties
• HyperLTL satisfiability is highly undecidable, \(\mathrm{HyperCTL}^*\) is even harder
• Extensions of HyperLTL for asynchronous hyperproperties

This page was built for publication: Bounded model checking for asynchronous hyperproperties

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