Efficient loop conditions for bounded model checking hyperproperties

DOI10.1007/978-3-031-30823-9_4MaRDI QIDQ6535341zbMATH OpenFDO

Authors Tzu-Han Hsu, César Sánchez, Sarai Sheinvald, Borzoo Bonakdarpour

Publication date 13 December 2023

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

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

Recommendations

• Bounded model checking for hyperproperties
• Bounded model checking for asynchronous hyperproperties
• Model checking algorithms for hyperproperties (invited paper)
• Model checking quantitative hyperproperties
• Verifying bounded subset-closed hyperproperties
• Computer Aided Verification
• Bounded model checking for all regular properties
• Accelerating bounded model checking of safety properties
• Bounded model checking with parametric data structures
• Model checking hyperproperties for Markov decision processes

Cites work

• scientific article; zbMATH DE number 3982506 (Why is no real title available?)
• scientific article; zbMATH DE number 2102704 (Why is no real title available?)
• A temporal logic for asynchronous hyperproperties
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Automata-theoretic techniques for modal logics of programs
• Bounded model checking for hyperproperties
• Bounded model checking using satisfiability solving
• Compositional model checking for multi-properties
• Gray-box monitoring of hyperproperties with an application to privacy
• Model checking quantitative hyperproperties
• Monitoring hyperproperties
• Propositional Dynamic Logic for Hyperproperties
• Rewriting-based runtime verification for alternation-free HyperLTL
• Software Verification of Hyperproperties Beyond k-Safety
• Synthesizing reactive systems from hyperproperties
• The existence of refinement mappings
• Verifying hyperliveness
• Witnessing secure compilation

Cited in

(1)

• Model checking quantitative hyperproperties

This page was built for publication: Efficient loop conditions for bounded model checking hyperproperties

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