Efficient loop conditions for bounded model checking hyperproperties

DOI10.1007/978-3-031-30823-9_4zbMATH Open1543.68217MaRDI QIDQ6535341FDOQ6535341

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

Publication date: 13 December 2023

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

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

• Title not available (Why is that?)
• The existence of refinement mappings
• Bounded model checking using satisfiability solving
• Automata-theoretic techniques for modal logics of programs
• Title not available (Why is that?)
• Witnessing secure compilation
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Model checking quantitative hyperproperties
• Bounded model checking for hyperproperties
• Verifying hyperliveness
• A temporal logic for asynchronous hyperproperties
• Monitoring hyperproperties
• Rewriting-Based Runtime Verification for Alternation-Free HyperLTL
• Gray-box monitoring of hyperproperties with an application to privacy
• Synthesizing reactive systems from hyperproperties
• Compositional model checking for multi-properties
• Propositional Dynamic Logic for Hyperproperties
• Software Verification of Hyperproperties Beyond k-Safety

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)