Zobrazeno 1 - 10
of 183
pro vyhledávání: '"Tentrup, A."'
Autor:
Jacobs, Swen, Perez, Guillermo A., Abraham, Remco, Bruyere, Veronique, Cadilhac, Michael, Colange, Maximilien, Delfosse, Charly, van Dijk, Tom, Duret-Lutz, Alexandre, Faymonville, Peter, Finkbeiner, Bernd, Khalimov, Ayrat, Klein, Felix, Luttenberger, Michael, Meyer, Klara, Michaud, Thibaud, Pommellet, Adrien, Renkin, Florian, Schlehuber-Caissier, Philipp, Sakr, Mouhammad, Sickert, Salomon, Staquet, Gaetan, Tamines, Clement, Tentrup, Leander, Walker, Adam
We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYN
Externí odkaz:
http://arxiv.org/abs/2206.00251
Publikováno v:
=In: Lahiri S., Wang C. (eds) Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science, vol 12225
We studied the hyperlogic HyperQPTL, which combines the concepts of trace relations and $\omega$-regularity. We showed that HyperQPTL is very expressive, it can express properties like promptness, bounded waiting for a grant, epistemic properties, an
Externí odkaz:
http://arxiv.org/abs/2101.07161
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
Externí odkaz:
http://arxiv.org/abs/2101.07109
Publikováno v:
In: Dillig I., Tasiran S. (eds) Computer Aided Verification. CAV 2019. Lecture Notes in Computer Science, vol 11561. Springer, Cham
HyperLTL is an extension of linear-time temporal logic for the specification of hyperproperties, i.e., temporal properties that relate multiple computation traces. HyperLTL can express information flow policies as well as properties like symmetry in
Externí odkaz:
http://arxiv.org/abs/2005.07425
We present RVHyper, a runtime verification tool for hyperproperties. Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. Specifications are given as formulas in the temporal log
Externí odkaz:
http://arxiv.org/abs/1906.00798
Verifying hyperproperties at runtime is a challenging problem as hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. It is necessary to store previously seen traces, because eve
Externí odkaz:
http://arxiv.org/abs/1905.13517
We study the reactive synthesis problem for hyperproperties given as formulas of the temporal logic HyperLTL. Hyperproperties generalize trace properties, i.e., sets of traces, to sets of sets of traces. Typical examples are information-flow policies
Externí odkaz:
http://arxiv.org/abs/1905.13511
Incremental determinization is a recently proposed algorithm for solving quantified Boolean formulas with one quantifier alternation. In this paper, we formalize incremental determinization as a set of inference rules to help understand the design sp
Externí odkaz:
http://arxiv.org/abs/1905.13411
Autor:
Jacobs, Swen, Bloem, Roderick, Colange, Maximilien, Faymonville, Peter, Finkbeiner, Bernd, Khalimov, Ayrat, Klein, Felix, Luttenberger, Michael, Meyer, Philipp J., Michaud, Thibaud, Sakr, Mouhammad, Sickert, Salomon, Tentrup, Leander, Walker, Adam
We report on the fifth reactive synthesis competition (SYNTCOMP 2018). We introduce four new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the evaluation scheme and the experimental setup of SYNTCOMP 2018. We gi
Externí odkaz:
http://arxiv.org/abs/1904.07736
Autor:
Tentrup, Leander, Rabe, Markus N.
Dependency quantified Boolean formulas (DQBF) is a logic admitting existential quantification over Boolean functions, which allows us to elegantly state synthesis problems in verification such as the search for invariants, programs, or winning region
Externí odkaz:
http://arxiv.org/abs/1808.08759