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

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

(4)

• Exploiting step semantics for efficient bounded model checking of asynchronous systems
• Model checking quantitative hyperproperties
• Efficient loop conditions for bounded model checking hyperproperties
• scientific article; zbMATH DE number 1629966 (Why is no real title available?)

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)