Synthesis from hyperproperties

DOI10.1007/S00236-019-00358-2zbMath1435.68194DBLPjournals/acta/FinkbeinerHLST20arXiv1905.13511OpenAlexW2994155569WikidataQ90444290 ScholiaQ90444290MaRDI QIDQ2303878

Bernd Finkbeiner, Philip Lukert, Leander Tentrup, Christopher Hahn, Marvin Stenger

Publication date: 6 March 2020

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1905.13511

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (5)

Program Repair for Hyperproperties ⋮ Explaining Hyperproperty Violations ⋮ Bounded model checking for hyperproperties ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ Model checking hyperproperties for Markov decision processes

Uses Software

• z3
• BoSy

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Monitoring hyperproperties
• Model Checking Information Flow in Reactive Systems
• Detecting Unrealizability of Distributed Fault-tolerant Systems
• Encodings of Bounded Synthesis
• Rewriting-Based Runtime Verification for Alternation-Free HyperLTL
• Synthesis of Asynchronous Systems
• Synthesis of Fault-Tolerant Distributed Systems
• The complexity of propositional linear temporal logics
• The First-Order Logic of Hyperproperties
• Automated Technology for Verification and Analysis
• A variant of a recursively unsolvable problem
• Model checking quantitative hyperproperties
• Synthesizing reactive systems from hyperproperties

This page was built for publication: Synthesis from hyperproperties