Bibliografías temáticas / Hyperproperties verification

Índice

  1. Artículos de revistas
  2. Tesis
  3. Capítulos de libros
  4. Actas de conferencias

Literatura académica sobre el tema "Hyperproperties verification"

Autor: Grafiati
Publicado: 11 de marzo de 2023
Última modificación: 19 de julio de 2025

Crea una cita precisa en los estilos APA, MLA, Chicago, Harvard y otros

Elija tipo de fuente:

Consulte las listas temáticas de artículos, libros, tesis, actas de conferencias y otras fuentes académicas sobre el tema "Hyperproperties verification".

Junto a cada fuente en la lista de referencias hay un botón "Agregar a la bibliografía". Pulsa este botón, y generaremos automáticamente la referencia bibliográfica para la obra elegida en el estilo de cita que necesites: APA, MLA, Harvard, Vancouver, Chicago, etc.

También puede descargar el texto completo de la publicación académica en formato pdf y leer en línea su resumen siempre que esté disponible en los metadatos.

Artículos de revistas sobre el tema "Hyperproperties verification"

1

Dardinier, Thibault, Anqi Li, and Peter Müller. "Hypra: A Deductive Program Verifier for Hyper Hoare Logic." Proceedings of the ACM on Programming Languages 8, OOPSLA2 (2024): 1279–308. http://dx.doi.org/10.1145/3689756.

Texto completo
Resumen
Hyperproperties relate multiple executions of a program and are useful to express common correctness properties (such as determinism) and security properties (such as non-interference). While there are a number of powerful program logics for the deductive verification of hyperproperties, their automation falls behind. Most existing deductive verification tools are limited to safety properties, but cannot reason about the existence of executions, for instance, to prove the violation of a safety property. Others support more flexible hyperproperties such as generalized non-interference, but have
Los estilos APA, Harvard, Vancouver, ISO, etc.
2

Beutner, Raven, and Bernd Finkbeiner. "Non-deterministic Planning for Hyperproperty Verification." Proceedings of the International Conference on Automated Planning and Scheduling 34 (May 30, 2024): 25–30. http://dx.doi.org/10.1609/icaps.v34i1.31457.

Texto completo
Resumen
Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes parts of the current state. Hyperproperties are properties that relate multiple paths of a system and can, e.g., capture security and information-flow policies. Popular logics for expressing temporal hyperproperties - such as HyperLTL - extend LTL by offering selective quantification over executions of a system. In this paper, we show that planning offers a powerful intermediate language for the automated verificati
Los estilos APA, Harvard, Vancouver, ISO, etc.
3

Correnson, Arthur, and Bernd Finkbeiner. "Coinductive Proofs for Temporal Hyperliveness." Proceedings of the ACM on Programming Languages 9, POPL (2025): 1568–95. https://doi.org/10.1145/3704889.

Texto completo
Resumen
Temporal logics for hyperproperties have recently emerged as an expressive specification technique for relational properties of reactive systems. While the model checking problem for such logics has been widely studied, there is a scarcity of deductive proof systems for temporal hyperproperties. In particular, hyperproperties with an alternation of universal and existential quantification over system executions are rarely supported. In this paper, we focus on hyperproperties of the form ∀ * ∃ * ψ, where ψ is a safety relation. We show that hyperproperties of this class – which includes many hy
Los estilos APA, Harvard, Vancouver, ISO, etc.
4

Baier, Christel. "Verification Column." ACM SIGLOG News 10, no. 2 (2023): 3. http://dx.doi.org/10.1145/3610392.3610393.

Texto completo
Resumen
Temporal logics for hyper properties provide an elegant way to express properties of sets of executions traces. In contrast to classical temporal logics like LTL or CTL, they can express relations of individual execution traces of a system. Among others, they can formalize information-flow principles and other security requirements that are not definable in LTL or CTL. The article by Bernd Finkbeiner provides an overview of temporal logics for hyperproperties. The first part provides an introduction tp HyperLTL and algorithmic problems (satisfiability, model checking, monitoring, synthesis). T
Los estilos APA, Harvard, Vancouver, ISO, etc.
5

Wang, Yu, Mojtaba Zarei, Borzoo Bonakdarpour, and Miroslav Pajic. "Statistical Verification of Hyperproperties for Cyber-Physical Systems." ACM Transactions on Embedded Computing Systems 18, no. 5s (2019): 1–23. http://dx.doi.org/10.1145/3358232.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
6

Finkbeiner, Bernd, Christopher Hahn, Marvin Stenger, and Leander Tentrup. "Efficient monitoring of hyperproperties using prefix trees." International Journal on Software Tools for Technology Transfer 22, no. 6 (2020): 729–40. http://dx.doi.org/10.1007/s10009-020-00552-5.

Texto completo
Resumen
Abstract Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other and are thus not monitorable by tools that consider computations in isolation. We present the monitoring approach implemented in the latest version of $$\text {RVHyper}$$ RVHyper , a runtime verification tool for hyperproperties. The input to the tool are specifications given in the temporal logic $$\text {HyperLTL}$$ HyperLTL , which extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. $$\text {RVHyper}$$ RVHyper processes executi
Los estilos APA, Harvard, Vancouver, ISO, etc.
7

Beutner, Raven, and Bernd Finkbeiner. "Predicate abstraction for hyperliveness verification." Formal Methods in System Design, July 16, 2025. https://doi.org/10.1007/s10703-025-00482-5.

Texto completo
Resumen
Abstract Temporal hyperproperties are system properties that relate multiple execution traces. In finite-state systems, temporal hyperproperties are supported by model-checking algorithms, and tools for general temporal logics like HyperLTL exist. In infinite-state systems, the analysis of temporal hyperproperties has, so far, been limited to k-safety properties, i.e., properties that stipulate the absence of a bad interaction between any k traces. In this paper, we present an automated method for the verification of $$\forall ^k\exists ^l$$ ∀ k ∃ l -safety properties in infinite-state systems
Los estilos APA, Harvard, Vancouver, ISO, etc.
8

Stucki, Sandro, César Sánchez, Gerardo Schneider, and Borzoo Bonakdarpour. "Gray-box monitoring of hyperproperties with an application to privacy." Formal Methods in System Design, February 2, 2021. http://dx.doi.org/10.1007/s10703-020-00358-w.

Texto completo
Resumen
AbstractRuntime verification is a complementary approach to testing, model checking and other static verification techniques to verify software properties. Monitorability characterizes what can be verified (monitored) at run time. Different definitions of monitorability have been given both for trace properties and for hyperproperties (properties defined over sets of traces), but these definitions usually cover only some aspects of what is important when characterizing the notion of monitorability. The first contribution of this paper is a refinement of classic notions of monitorability both f
Los estilos APA, Harvard, Vancouver, ISO, etc.
9

Anand, Mahathi, Vishnu Murali, Ashutosh Trivedi, and Majid Zamani. "Verification of Hyperproperties for Dynamical Systems via Barrier Certificates." IEEE Transactions on Automatic Control, 2024, 1–16. http://dx.doi.org/10.1109/tac.2024.3384448.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
10

Beutner, Raven, and Bernd Finkbeiner. "AutoHyper: leveraging language inclusion checking for hyperproperty model-checking." International Journal on Software Tools for Technology Transfer, May 6, 2025. https://doi.org/10.1007/s10009-025-00801-5.

Texto completo
Resumen
Abstract Hyperproperties are system properties that relate multiple execution traces, and naturally occur, e.g., in information-flow control, knowledge, robustness, mutation testing, path planning, and causality checking. HyperLTL is a temporal logic that can express complex temporal hyperproperties by extending LTL with quantification over execution traces. Thus far, complete model-checking tools for HyperLTL have been limited to alternation-free formulas, i.e., formulas that use only universal or only existential trace quantification. In this paper, we present , an explicit-state automata-ba
Los estilos APA, Harvard, Vancouver, ISO, etc.

Tesis sobre el tema "Hyperproperties verification"

1

Pasqua, Michele. "Hyper Static Analysis of Programs - An Abstract Interpretation-Based Framework for Hyperproperties Verification." Doctoral thesis, 2019. http://hdl.handle.net/11562/995302.

Texto completo
Resumen
In the context of systems security, information flows play a central role. Unhandled information flows potentially leave the door open to very dangerous types of security attacks, such as code injection or sensitive information leakage. Information flows verification is based on a notion of dependency between a system’s objects, which requires specifications expressing relations between different executions of a system. Specifications of this kind, called hyperproperties, go beyond classic trace properties, defined in terms of predicate over single executions. The problem of trace properties v
Los estilos APA, Harvard, Vancouver, ISO, etc.

Capítulos de libros sobre el tema "Hyperproperties verification"

1

Finkbeiner, Bernd, Christopher Hahn, Marvin Stenger, and Leander Tentrup. "Monitoring Hyperproperties." In Runtime Verification. Springer International Publishing, 2017. http://dx.doi.org/10.1007/978-3-319-67531-2_12.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
2

Chalupa, Marek, and Thomas A. Henzinger. "Monitoring Hyperproperties with Prefix Transducers." In Runtime Verification. Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-44267-4_9.

Texto completo
Resumen
AbstractHyperproperties are properties that relate multiple execution traces. Previous work on monitoring hyperproperties focused on synchronous hyperproperties, usually specified in HyperLTL. When monitoring synchronous hyperproperties, all traces are assumed to proceed at the same speed. We introduce (multi-trace) prefix transducers and show how to use them for monitoring synchronous as well as, for the first time, asynchronous hyperproperties. Prefix transducers map multiple input traces into one or more output traces by incrementally matching prefixes of the input traces against expressions similar to regular expressions. The prefixes of different traces which are consumed by a single matching step of the monitor may have different lengths. The deterministic and executable nature of prefix transducers makes them more suitable as an intermediate formalism for runtime verification than logical specifications, which tend to be highly non-deterministic, especially in the case of asynchronous hyperproperties. We report on a set of experiments about monitoring asynchronous version of observational determinism.
Los estilos APA, Harvard, Vancouver, ISO, etc.
3

Beutner, Raven, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger. "Second-Order Hyperproperties." In Computer Aided Verification. Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-37703-7_15.

Texto completo
Resumen
AbstractWe introduce Hyper2LTL, a temporal logic for the specification of hyperproperties that allows for second-order quantification over sets of traces. Unlike first-order temporal logics for hyperproperties, such as HyperLTL, Hyper2LTL can express complex epistemic properties like common knowledge, Mazurkiewicz trace theory, and asynchronous hyperproperties. The model checking problem of Hyper2LTL is, in general, undecidable. For the expressive fragment where second-order quantification is restricted to smallest and largest sets, we present an approximate model-checking algorithm that computes increasingly precise under- and overapproximations of the quantified sets, based on fixpoint iteration and automata learning. We report on encouraging experimental results with our model-checking algorithm, which we implemented in the tool .
Los estilos APA, Harvard, Vancouver, ISO, etc.
4

Hahn, Christopher. "Algorithms for Monitoring Hyperproperties." In Runtime Verification. Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-32079-9_5.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
5

Finkbeiner, Bernd, Christopher Hahn, and Hazem Torfah. "Model Checking Quantitative Hyperproperties." In Computer Aided Verification. Springer International Publishing, 2018. http://dx.doi.org/10.1007/978-3-319-96145-3_8.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
6

Finkbeiner, Bernd, Christopher Hahn, Jana Hofmann, and Leander Tentrup. "Realizing $$\omega $$-regular Hyperproperties." In Computer Aided Verification. Springer International Publishing, 2020. http://dx.doi.org/10.1007/978-3-030-53291-8_4.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
7

Dobe, Oyendrila, Stefan Schupp, Ezio Bartocci, et al. "Lightweight Verification of Hyperproperties." In Automated Technology for Verification and Analysis. Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-45332-8_1.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
8

Finkbeiner, Bernd, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. "Synthesizing Reactive Systems from Hyperproperties." In Computer Aided Verification. Springer International Publishing, 2018. http://dx.doi.org/10.1007/978-3-319-96145-3_16.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
9

Beutner, Raven, and Bernd Finkbeiner. "Software Verification of Hyperproperties Beyond k-Safety." In Computer Aided Verification. Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-031-13185-1_17.

Texto completo
Resumen
AbstractTemporal hyperproperties are system properties that relate multiple execution traces. For (finite-state) hardware, temporal hyperproperties are supported by model checking algorithms, and tools for general temporal logics like HyperLTL exist. For (infinite-state) software, the analysis of temporal hyperproperties has, so far, been limited to k-safety properties, i.e., properties that stipulate the absence of a bad interaction between any k traces. In this paper, we present an automated method for the verification of $$\forall ^k\exists ^l$$ ∀ k ∃ l -safety properties in infinite-state systems. A $$\forall ^k\exists ^l$$ ∀ k ∃ l -safety property stipulates that for any k traces, there existl traces such that the resulting $$k+l$$ k + l traces do not interact badly. This combination of universal and existential quantification enables us to express many properties beyond k-safety, including, for example, generalized non-interference or program refinement. Our method is based on a strategy-based instantiation of existential trace quantification combined with a program reduction, both in the context of a fixed predicate abstraction. Notably, our framework allows for mutual dependence of strategy and reduction.
Los estilos APA, Harvard, Vancouver, ISO, etc.
10

Baumeister, Jan, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. "A Temporal Logic for Asynchronous Hyperproperties." In Computer Aided Verification. Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-81685-8_33.

Texto completo
Resumen
AbstractHyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics are synchronous in the sense that all traces proceed at the same speed and are evaluated at the same position. This precludes the use of these logics to analyze systems whose traces can proceed at different speeds and allow that different traces take stuttering steps independently. To solve this problem in this paper, we propose an asynchronous variant of HyperLTL. On the negative side, we show that the model-checking problem for this variant is undecidable. On the positive side, we identify a decidable fragment which covers a rich set of formulas with practical applications. We also propose two model-checking algorithms that reduce our problem to the HyperLTL model-checking problem in the synchronous semantics.
Los estilos APA, Harvard, Vancouver, ISO, etc.

Actas de conferencias sobre el tema "Hyperproperties verification"

1

Long, Teng, and Guoqing Yao. "Verification for Security-Relevant Properties and Hyperproperties." In 2015 IEEE 12th Intl. Conf. on Ubiquitous Intelligence and Computing, 2015 IEEE 12th Intl. Conf. on Autonomic and Trusted Computing and 2015 IEEE 15th Intl. Conf. on Scalable Computing and Communications and its Associated Workshops (UIC-ATC-ScalCom). IEEE, 2015. http://dx.doi.org/10.1109/uic-atc-scalcom-cbdcom-iop.2015.101.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
2

Pinisetty, Srinivas, Gerardo Schneider, and David Sands. "Runtime verification of hyperproperties for deterministic programs." In ICSE '18: 40th International Conference on Software Engineering. ACM, 2018. http://dx.doi.org/10.1145/3193992.3193995.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
3

Anand, Mahathi, Vishnu Murali, Ashutosh Trivedi, and Majid Zamani. "Formal verification of hyperproperties for control systems." In CPS-IoT Week '21: Cyber-Physical Systems and Internet of Things Week 2021. ACM, 2021. http://dx.doi.org/10.1145/3457335.3461715.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
4

Agrawal, Shreya, and Borzoo Bonakdarpour. "Runtime Verification of k-Safety Hyperproperties in HyperLTL." In 2016 IEEE 29th Computer Security Foundations Symposium (CSF). IEEE, 2016. http://dx.doi.org/10.1109/csf.2016.24.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
5

Zhang, Yusha, Ziyuan Zhu, Yuxin Liu, Zhongkai Tong, Wenjing Cai, and Dan Meng. "A Formal Verification Methodology for Cache Architectures Based on Noninterference Hyperproperties." In 2024 27th International Conference on Computer Supported Cooperative Work in Design (CSCWD). IEEE, 2024. http://dx.doi.org/10.1109/cscwd61410.2024.10580574.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
Ofrecemos descuentos en todos los planes premium para autores cuyas obras están incluidas en selecciones literarias temáticas. ¡Contáctenos para obtener un código promocional único!

Pasar a la bibliografía