From LTL to rLTL monitoring: improved monitorability through robust semantics [0.03%]
从LTL到rLTL监控：通过健壯语义提高可監控性
Corto Mascle,Daniel Neider,Maximilian Schwenger et al.
Corto Mascle et al.
Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (...
Maurice H Ter Beek,Annabelle McIver
Maurice H Ter Beek
Michael Blondin,Javier Esparza,Stefan Jaax et al.
Michael Blondin et al.
Population protocols are a well established model of computation by anonymous, identical finite-state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. Th...
Maurice H Ter Beek,Annabelle McIver
Maurice H Ter Beek
Incremental column-wise verification of arithmetic circuits using computer algebra [0.03%]
基于计算机代数的算术电路列式增量验证方法
Daniela Kaufmann,Armin Biere,Manuel Kauers
Daniela Kaufmann
Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean p...
Yulia Demyanova,Thomas Pani,Helmut Veith et al.
Yulia Demyanova et al.
We study empirical metrics for software source code, which can predict the performance of verification tools on specific types of software. Our metrics comprise variable usage patterns, loop patterns, as well as indicators of control-flow c...
Shield synthesis [0.03%]
盾牌合成
Bettina Könighofer,Mohammed Alshiekh,Roderick Bloem et al.
Bettina Könighofer et al.
Shield synthesis is an approach to enforce safety properties at runtime. A shield monitors the system and corrects any erroneous output values instantaneously. The shield deviates from the given outputs as little as it can and recovers to h...
Para [Formula: see text] : parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms [0.03%]
Para [公式见PDF]: 带参数路径约简、加速和SMT在门限保护的分布式算法中求可达性问题的方法中阈值守护的分布式算法中的可达性分析方法
Igor Konnov,Marijana Lazić,Helmut Veith et al.
Igor Konnov et al.
Automatic verification of threshold-based fault-tolerant distributed algorithms (FTDA) is challenging: FTDAs have multiple parameters that are restricted by arithmetic conditions, the number of processes and faults is parameterized, and the...
Roderick Bloem,Goerschwin Fey,Fabian Greif et al.
Roderick Bloem et al.
Constructing good test cases is difficult and time-consuming, especially if the system under test is still under development and its exact behavior is not yet fixed. We propose a new approach to compute test strategies for reactive systems ...
Monitoring hyperproperties [0.03%]
监控超属性
Bernd Finkbeiner,Christopher Hahn,Marvin Stenger et al.
Bernd Finkbeiner et al.
Hyperproperties, such as non-interference and observational determinism, relate multiple system executions to each other. They are not expressible in standard temporal logics, like LTL, CTL, and CTL*, and thus cannot be monitored with stand...