×

A survey of challenges for runtime verification from advanced application domains (beyond software). (English) Zbl 1425.68268

Summary: Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abadi M, Andersen DG (2016) Learning to protect communications with adversarial neural cryptography. Technical Report CoRR. arXiv:1610.06918
[2] Abbas, H.; Fainekos, GE; Sankaranarayanan, S.; Ivancic, F.; Gupta, A., Probabilistic temporal logic falsification of cyber-physical systems, ACM Trans Embed Comput Syst, 12, 95:1-95:30 (2013)
[3] Abbas H, Winn A, Fainekos GE, Julius AA (2014) Functional gradient descent method for metric temporal logic specifications. In: Proceedings of the American control conference (ACC’14). IEEE, pp 2312-2317
[4] Aceto L, Achilleos A, Francalanza A, Ingólfsdóttir A (2017) Monitoring for silent actions. In: Proceedings of the 37th IARCS annual conference on foundations of software technology and theoretical computer science, (FSTTCS’17), volume 93 of LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp 7:1-7:14 · Zbl 1491.68104
[5] Aceto L, Achilleos A, Francalanza A, Ingólfsdóttir A (2018) A framework for parameterized monitorability. In: Proceedings of the 21st Int’l conference on foundations of software science and computation structures (FOSSACS’18), volume 10803 of LNCS. Springer, pp 203-220 · Zbl 1504.68136
[6] Aceto L, Achilleos A, Francalanza A, Ingólfsdóttir A, Kjartansson SÖ (2017) On the complexity of determinizing monitors. In: Proceedings of the 22nd Int’l conference on implementation and application of automata (CIAA’17), volume 10329 of LNCS. Springer, pp 1-13 · Zbl 1489.68149
[7] Aceto, Luca; Achilleos, Antonis; Francalanza, Adrian; Ingólfsdóttir, Anna; Lehtinen, Karoliina, Adventures in monitorability: from branching to linear time and back again, Proceedings of the ACM on Programming Languages, 3, 1-29 (2019)
[8] Aceto L, Cassar I, Francalanza A, Ingólfsdóttir A (2018) On runtime enforcement via suppressions. In: Schewe S, Zhang L (eds) 29th International conference on concurrency theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, pp 34:1-34:17 · Zbl 1520.68069
[9] Agarwal S, Mozafari B, Panda A, Milner H, Madden S, Stoica I (2013) BlinkDB: Queries with bounded errors and bounded response times on very large data. In: Proceedings of the 8th ACM European conference on computer systems (EuroSys ’13). ACM, pp 29-42
[10] Ahrendt W, Pace GJ, Schneider G (2018) Smart contracts: a killer application for deductive source code verification. In: Principled software development—essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Springer, pp 1-18
[11] Akazaki T, Hasuo I (2015) Time robustness in MTL and expressivity in hybrid system falsification. In: Proceedings of the 27th Int’l conference on computer aided verification (CAV’15), volume 9207 of LNCS. Springer, pp 356-374 · Zbl 1381.68142
[12] Alagar, S.; Venkatesan, S., Techniques to tackle state explosion in global predicate detection, IEEE Trans Softw Eng (TSE), 27, 704-714 (2001)
[13] Alberti, M.; Chesani, F.; Gavanelli, M.; Lamma, E.; Mello, P.; Torroni, P., Verifiable agent interaction in abductive logic programming: the SCIFF framework, ACM Trans Comput Log, 9, 29:1-29:43 (2008) · Zbl 1367.68273
[14] Althoff M (2013) Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings the 16th Int’l conference on hybrid systems computation and control (HSCC’13). ACM, pp 173-182 · Zbl 1362.93011
[15] Alur, R.; Feder, T.; Henzinger, TA, The benefits of relaxing punctuality, J ACM, 43, 116-146 (1996) · Zbl 0882.68021
[16] Anicic D, Fodor P, Rudolph S, Stühmer R, Stojanovic N, Studer R (2010) A rule-based language for complex event processing and reasoning. In: Proceedings of the 4th Int’l conference on web reasoning and rule systems (RR’10), volume 6333 of LNCS. Springer, pp. 42-57
[17] Annapureddy Y, Liu C, Fainekos G, Sankaranarayanan S (2011) S-taliro: A tool for temporal logic falsification for hybrid systems. In: Proceedings of the 17th Int’l conference on tools and algorithms for the construction and analysis of systems (TACAS’11), volume 6605 of LNCS. Springer, pp 254-257 · Zbl 1316.68069
[18] Annapureddy YSR, Fainekos (GE) (2010) Ant colonies for temporal logic falsification of hybrid systems. In: Proceedings of the 36th annual conference on IEEE industrial electronics society (IECON’10)
[19] Antignac T, Sands D, Schneider G (2017) Data minimisation: a language-based approach. In: Proceedings of the 32nd IFIP TC Int’l conference on ICT system security and privacy protection (IFIP SEC’17), volume 502 of IFIP advances in information and communication technology (AICT). Springer, pp 442-456
[20] Arackaparambil C, Brody J, Chakrabarti A (2009) Functional monitoring without monotonicity. In: Proceedings of the 36th Int’l colloquium on automata, languages and programming: Part I (ICALP’09), volume 5555 of LNCS. Springer, pp 95-106 · Zbl 1248.68085
[21] Arasu, A.; Babu, S.; Widom, J., The CQL continuous query language: semantic foundations and query execution, VLDB J, 15, 121-142 (2006)
[22] ARM, Cambridge, England. ARM CoreSight Architecture Specification, 2.0 edition, Sept. 2013
[23] Armbrust, M.; Fox, A.; Griffith, R.; Joseph, AD; Katz, RH; Konwinski, A.; Lee, G.; Patterson, DA; Rabkin, A.; Stoica, I.; Zaharia, M., A view of cloud computing, Commun ACM, 53, 50-58 (2010)
[24] Arshad S, Kharraz A, Robertson W (2016) Identifying extension-based ad injection via fine-grained web content provenance. In: Proceedings of the 19th Int’l symposium on research in attacks, intrusions, and defenses (RAID’16), volume 9854 of LNCS. Springer, pp 415-436
[25] Asarin, E.; Caspi, P.; Maler, O., Timed regular expressions, J ACM, 49, 172-206 (2002) · Zbl 1323.68335
[26] Asarin, E.; Maler, O.; Pnueli, A., Reachability analysis of dynamical systems having piecewise-constant derivatives, Theor Comput Sci, 138, 35-65 (1995) · Zbl 0884.68050
[27] Asarin, E.; Mysore, V.; Pnueli, A.; Schneider, G., Low dimensional hybrid systems-decidable, undecidable, don’t know, Inf Comput, 211, 138-159 (2012) · Zbl 1279.68127
[28] Asarin E, Schneider G, Yovine S (2001) On the decidability of the reachability problem for planar differential inclusions. In: 4th International workshop on hybrid systems: computation and control (HSCC’01), number 2034 in LNCS. Springer, pp 89-104 · Zbl 0991.93009
[29] Asarin, E.; Schneider, G.; Yovine, S., Algorithmic analysis of polygonal hybrid systems. Part I: reachability, Theor Comput Sci, 379, 231-265 (2007) · Zbl 1121.68071
[30] Attard DP, Francalanza A (2016) A monitoring tool for a branching-time logic. In: Proceedings of the 16th Int’l conference on runtime verification (RV’16), volume 10012 of LNCS. Springer, pp 473-481
[31] Attard DP, Francalanza A (2017) Trace partitioning and local monitoring for asynchronous components. In: Proceedings of the 15th Int’l conference on software engineering and formal methods (SEFM’17), volume 10469 of LNCS. Springer, pp 219-235
[32] Attiya H, Welch JL (2004) Distributed computing: fundamentals, simulations and advanced topics. Wiley, Amsterdam · Zbl 0910.68077
[33] Atzei N, Bartoletti M, Cimoli T (2017) A survey of attacks on Ethereum smart contracts (SoK). In: Proceedings of the 6th Int’l conference on principles of security and trust (POST’17), volume 10204 of LNCS. Springer, pp 164-186
[34] Austin TH, Flanagan C (2010) Permissive dynamic information flow analysis. In: Proceedings of the workshop on programming languages and analysis for security (PLAS’10). ACM, pp 1-12
[35] Austin TH, Flanagan C (2012) Multiple facets for dynamic information flow. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symp, on principles of programming languages (POPL’12). ACM, pp 165-178 · Zbl 1321.68034
[36] Azzopardi, Shaun; Ellul, Joshua; Pace, Gordon J., Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond, 113-137 (2018), Cham
[37] Azzopardi, S.; Pace, GJ; Schapachnik, F.; Schneider, G., Contract automata: an operational view of contracts between interactive parties, Artif Intell Law, 24, 203-243 (2016)
[38] Babcock B, Babu S, Datar M, Motwani R, Widom J (2002) Models and issues in data stream systems. In: Proceedings of the 21st ACM SIGMOD-SIGACT-SIGART symposium on principles of database systems (PODS’02). ACM, pp 1-16
[39] Babcock B, Olston C (2003) Distributed top-k monitoring. In: Proceedings of the 2003 ACM SIGMOD Int’l conference on management of data (SIGMOD’03). ACM, pp 28-39
[40] Baker, HC; Hewitt, C., The incremental garbage collection of processes, SIGPLAN Not, 12, 55-59 (1977)
[41] Barany G, Signoles J (2017) Hybrid information flow analysis for real-world C code. In: Proceedings of the 11th Int’l conference on tests and proofs (TAP’17), LNCS. Springer, pp 23-40
[42] Barre B, Klein M, Boivin S-M, Ollivier P-A, Hallé S (2012) MapReduce for parallel trace validation of LTL properties. In: Proceedings of the 17th Int’l conference on runtime verification (RV’12), volume 7687 of LNCS. Springer, pp 184-198
[43] Bartocci, E.; Aydin-Gol, E.; Haghighi, I.; Belta, C., A formal methods approach to pattern recognition and synthesis in reaction diffusion networks, IEEE Trans Control Netw Syst, 5, 308-320 (2018) · Zbl 1507.92031
[44] Bartocci E, Bortolussi L, Loreti M, Nenzi L (2017) Monitoring mobile and spatially distributed cyber-physical systems. In: Proceedings of the 15th ACM-IEEE international conference on formal methods and models for system design (MEMOCODE’17). ACM, pp 146-155 · Zbl 07471693
[45] Bartocci, E.; Bortolussi, L.; Nenzi, L.; Sanguinetti, G., System design of stochastic models using robustness of temporal properties, Theor Comput Sci, 587, 3-25 (2015) · Zbl 1327.68147
[46] Bartocci E, Deshmukh JV, Donzé A, Fainekos GE, Maler O, Nickovic D, Sankaranarayanan S (2018) Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Lectures on runtime verification—introductory and advanced topics, volume 10457 of LNCS. Springer, pp 135-175
[47] Bartocci E, Falcone Y (eds) (2018) Lectures on runtime verification—introductory and advanced topics, volume 10457 of lecture notes in computer science. Springer
[48] Bartocci E, Ferrére T, Manjunath N, Nickovic D (2018) Localizing faults in Simulink/Stateflow models with STL. In: Proceedings of the 21st ACM Int’l conference on hybrid systems computation and control (HSCC’18). ACM, pp 197-206 · Zbl 1409.68168
[49] Bartocci E, Grosu R (2013) Monitoring with uncertainty. In: Proceedings 3rd Int’l workshop on hybrid autonomous systems, volume 124 of theoretical computer science. Open Publishing Association, pp 1-4
[50] Bartocci, Ezio; Grosu, Radu; Karmarkar, Atul; Smolka, Scott A.; Stoller, Scott D.; Zadok, Erez; Seyster, Justin, Adaptive Runtime Verification, 168-182 (2013), Berlin, Heidelberg
[51] Bartocci, E.; Liò, P., Computational modeling, formal analysis, and tools for systems biology, PLoS Comput Biol, 12, e1004591 (2016)
[52] Basin D, Bhatt B, Traytel D (2018) Optimal proofs for linear temporal logic on lasso words. In: Proceedings of the 16th Int’l symposium on automated technology for verification and analysis (ATVA’18), volume 11138 of LNCS. Springer · Zbl 1517.68222
[53] Basin, D.; Caronni, G.; Ereth, S.; Harvan, M.; Klaedtke, F.; Mantel, H., Scalable offline monitoring of temporal specifications, Formal Methods Syst Des, 49, 75-108 (2016) · Zbl 1380.68268
[54] Basin D, Klaedtke F, Marinovic S, Zălinescu E (2013) Monitoring compliance policies over incomplete and disagreeing logs. In: Proceedings of the 4th Int’l conference on runtime verification (RV’13), volume 8174 of LNCS. Springer, pp 151-167
[55] Basin D, Klaedtke F, Zalinescu E (2017) The MonPoly monitoring tool. In: An international workshop on competitions, usability, benchmarks, evaluation, and standardisation for runtime verification tools (RV-CuBES 2017), volume 3 of Kalpa Publications in Computing. EasyChair, pp 19-28
[56] Basin D, Krstić S, Traytel D (2017) Almost event-rate indepedent monitoring of metric dynamic logic. In: Proceedings of the 17th Int’l conference on runtime verification (RV’17), volume 10548 of LNCS. Springer, pp 85-102
[57] Basin DA, Bhatt BN, Traytel D (2017) Almost event-rate independent monitoring of metric temporal logic. In: Proceedings of the 23rd Int’l conference on tools and algorithms for the construction and analysis of systems (TACAS’17): Part II, volume 10206 of LNCS. Springer, pp 94-112 · Zbl 1452.68278
[58] Basin DA, Caronni G, Ereth S, Harvan M, Klaedtke F, Mantel H (2014) Scalable offline monitoring. In: Proceedings of 14th Int’l. conference on runtime verification (RV’14), volume 8734 of LNCS. Springer, pp 31-47 · Zbl 1380.68268
[59] Basin DA, Harvan M, Klaedtke F, Zalinescu E (2011) MONPOLY: Monitoring usage-control policies. In: Proceedings of the second Int’l conference on runtime verification (RV’11), volume 7186 of LNCS. Springer, pp 360-364
[60] Basin DA, Klaedtke F, Marinovic S, Zalinescu E (2012) Monitoring compliance policies over incomplete and disagreeing logs. In: Proceedings of the third Int’l conference on runtime verification (RV’12), volume 7687 of LNCS. Springer, pp 151-167
[61] Basin, DA; Klaedtke, F.; Marinovic, S.; Zalinescu, E., Monitoring of temporal first-order properties with aggregations, Formal Methods Syst Des, 46, 262-285 (2015) · Zbl 1323.68362
[62] Basin, D.; Klaedtke, F.; Müller, S.; Zălinescu, E., Monitoring metric first-order temporal properties, J ACM, 62, 15 (2015) · Zbl 1333.68177
[63] Basin DA, Klaedtke F, Zalinescu E (2015) Failure-aware runtime verification of distributed systems. In: Proceedings of the 35th IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS’15), volume 45 of Leibniz international proceedings in informatics (LIPIcs), Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp 590-603 · Zbl 1366.68010
[64] Basin DA, Klaedtke F, Zalinescu E (2017) Runtime verification of temporal properties over out-of-order data streams. In: Proceedings of the 29th Int’l conference on computer aided verification (CAV’17), volume 10426 of LNCS. Springer, pp 356-376 · Zbl 1494.68160
[65] Bauer AK, Falcone Y (2012) Decentralised LTL monitoring. In: Proceedings of the 18th Int’l symposium on formal methods (FM’12), volume 7436 of LNCS. Springer, pp 85-100 · Zbl 1372.68163
[66] Bauer, AK; Falcone, Y., Decentralised LTL monitoring, Formal Methods Syst Des, 48, 49-93 (2016) · Zbl 1392.68229
[67] Bauer, AK; Leucker, M.; Schallhart, C., Runtime verification for LTL and TLTL, ACM Trans Softw Eng Methodol, 20, 14:1-14:64 (2011)
[68] Bauer L, Cai S, Jia L, Passaro T, Stroucken M, Tian Y (2015) Run-time monitoring and formal analysis of information flows in chromium. In: Proceedings of the 22nd annual network and distributed system security symposium (NDSS’15). The Internet Society
[69] BBC Technology. Ransomware cyber-attack threat escalating—Europol (2017). https://www.bbc.com/news/technology-39913630
[70] Belta C, Yordanov B, Gol EA (2017) Formal methods for discrete-time dynamical systems. Springer, Berlin · Zbl 1409.93003
[71] Bemporad, A.; Morari, M., Control of systems integrating logic, dynamics, and constraints, Automatica, 35, 407-427 (1999) · Zbl 1049.93514
[72] Bersani MM, Bianculli D, Ghezzi C, Krstic S, Pietro PS (2016) Efficient large-scale trace checking using MapReduce. In: Proceedings of the 38th Int’l conference on software engineering (ICSE’16). ACM, pp 888-898
[73] Bessani A, Santos M, ao Felix J, Neves N, Correia M (2013) On the efficiency of durable state machine replication. In: Proceedings of the 2013 USENIX conference on annual technical conference (ATC’13). USENIX Association, pp 169-180
[74] Besson F, Bielova N, Jensen TP (2016) Hybrid monitoring of attacker knowledge. In: Proceedings of the IEEE 29th computer security foundations symposium (CSF’16). IEEE, pp 225-238
[75] Beyer B, Ewaschuk R (2016) Monitoring distributed systems. O’Reilly Media Inc, Cambridge
[76] Bhargavan K, Swamy N, Zanella-Béguelin S, Delignat-Lavaud A, Fournet C, Gollamudi A, Gonthier G, Kobeissi N, Kulatova N, Rastogi A, Sibut-Pinote T (2016) Formal verification of smart contracts. In: Proceedings of the 2016 ACM workshop on programming languages and analysis for security (PLAS’16). ACM Press, pp 91-96
[77] Bianculli D, Ghezzi C, Krstic S (2014) Trace checking of metric temporal logic with aggregating modalities using MapReduce. In: Proceedings of the 12th Int’l conference on software engineering and formal methods (SEFM’14), volume 8702 of LNCS. Springer, pp 144-158
[78] Bielova N, Rezk T (Apr. 2016) A taxonomy of information flow monitors. In: Proceedings of the 7th Int’l conference on principles of security and trust (POST’16), volume 9635 of LNCS. Springer, pp 46-67
[79] Bonakdarpour B, Fraigniaud P, Rajsbaum S, Travers C (2016) Challenges in fault-tolerant distributed runtime verification. In: Proceedings of the 7th Int’l symposium on leveraging applications of formal methods, verification and validation: foundational techniques (ISoLA’16): Part II, volume 9952 of LNCS. Springer, pp 363-370
[80] Bonakdarpour B, Sánchez C, Schneider G (2018) Monitoring hyperproperties by combining static analysis and runtime verification. In: 8th International symposium on leveraging applications of formal methods, verification and validation—track: a broader view on verification: from static to runtime and back (ISoLA’18, part II), volume 11245 of LNCS. Springer, pp 8-27
[81] Bolosky WJ, Bradshaw D, Haagens RB, Kusters NP, Li P (2011) Paxos replicated state machines as the basis of a high-performance data store. In: Proceedings of the 8th USENIX conference on networked systems design and implementation (NSDI’11). USENIX Association, pp 141-154
[82] Bortolussi L, Milios D, Guido S (2015) U-Check: Model checking and parameter synthesis under uncertainty. In: Proceedings of the 12th Int’l. conference on quantitative evaluation of systems (QEST’15), volume 9259 of LNCS. Springer, pp 89-104
[83] Boyer RS, Moore JS (1991) Automated reasoning: essays in Honor of Woody Bledsoe, chapter MJRTY—a fast majority vote algorithm. Springer, pp 105-117 · Zbl 0751.68002
[84] Buiras P, Vytiniotis D, Russo A (2015) Hlio: Mixing static and dynamic typing for information-flow control in haskell. In: Proceedings of the 20th ACM SIGPLAN Int’l conference on functional programming (ICFP’15). ACM, pp 289-301 · Zbl 1360.68316
[85] Bundala D, Ouaknine J (2014) On the complexity of temporal-logic path checking. In: Proceedings of 41st Int’l colloquium on automata, languages, and programming (ICALP’14). Part II, volume 8573 of LNCS. Springer, pp 86-97 · Zbl 1410.68219
[86] Bünzli A, Höfler S (2010) Controlling ambiguities in legislative language. In: Proceedings of the Int’l workshop on controlled natural language (CNL’10), volume 7175 of LNCS. Springer, pp 21-42
[87] Burrows M (2006) The chubby lock service for loosely-coupled distributed systems. In: Proceedings of the 7th symposium on operating systems design and implementation (OSDI’06). USENIX Association, pp 335-350
[88] Buterin V (2017) A next generation smart contract and decentralized application platform. Ethereum White Paper. Available online from https://github.com/ethereum/wiki/wiki/White-Paper
[89] Camilleri JJ, Haghshenas MR, Schneider G (2018) A web-based tool for analysing normative documents in English. In: Proceedings of the the 33rd ACM/SIGAPP symposium on applied computing—software verification and testing track (SAC-SVT’18). ACM
[90] Camilleri JJ, Pace GJ, Rosner M (2010) Controlled natural language in a game for legal assistance. In: Proceedings of the 2nd Int’l workshop on controlled natural language (CNL’10), volume 7175 of LNCS. Springer, pp 137-153
[91] Camilleri JJ, Paganelli G, Schneider G (2014) A CNL for contract-oriented diagrams. In: Proceedings of the 4th Int’l workshop on controlled natural language (CNL’14), volume 8625 of LNCS. Springer, pp 135-146
[92] Carbone, P.; Katsifodimos, A.; Ewen, S.; Markl, V.; Haridi, S.; Tzoumas, K., Apache \(flink^{{\rm TM}}\): stream and batch processing in a single engine, IEEE Data Eng Bull, 38, 28-38 (2015)
[93] Cassar I, Francalanza A (2015) Runtime adaptation for actor systems. In: Proceedings of the 6th Int’l conference on runtime verification (RV’15), volume 9333 of LNCS. Springer, pp 38-54
[94] Cassar, Ian; Francalanza, Adrian, On Implementing a Monitor-Oriented Programming Framework for Actor Systems, 176-192 (2016), Cham
[95] Cassar, Ian; Francalanza, Adrian; Said, Simon, Improving Runtime Overheads for detectEr, Electronic Proceedings in Theoretical Computer Science, 178, 1-8 (2015)
[96] Castro, M.; Liskov, B., Practical byzantine fault tolerance and proactive recovery, ACM Trans Comput Syst, 20, 398-461 (2002)
[97] Cavoukian A (2009) Privacy by design: the 7 foundational principles. In: Information and privacy commissioner of Ontario, Canada
[98] Chakarov A, Sankaranarayanan S, Fainekos GE (2011) Combining time and frequency domain specifications for periodic signals. In: Proceedings of the 2nd Int’l conference on runtime verification (RV’11), volume 7186 of LNCS. Springer, pp 294-309
[99] Chang E, Manna Z, Pnueli A (1992) Characterization of temporal property classes. In: Proceedings of the 19th Int’l colloquium on automata, languages and programming (ICALP’92), volume 623 of LNCS. Springer, pp 474-486 · Zbl 1425.68252
[100] Chauhan H, Garg VK, Natarajan A, Mittal N (2013) A distributed abstraction algorithm for online predicate detection. In: Proceedings of the 32nd IEEE symposium on reliable distributed systems, (SRDS’13). IEEE, pp 101-110
[101] Chen F, Roşu G (2009) Parametric trace slicing and monitoring. In: Proceedings of the 15th Int’l conference on tools and algorithms for the construction and analysis of systems (TACAS’09), volume 5505 of LNCS. Springer, pp 246-261 · Zbl 1234.68073
[102] Chen X, Ábrahám E, Sankaranarayanan S (2013) Flow*: an analyzer for non-linear hybrid systems. In: Proceedings of the 25th Int’l conference on computer aided verification (CAV’13), volume 8044 of LNCS. Springer, pp 258-263
[103] Clarkson, MR; Schneider, FB, Hyperproperties, J Comput Secur, 18, 1157-1210 (2010)
[104] Colombo C, Ellul J, Pace GJ (2018) Contracts over smart contracts: recovering from violations dynamically. In: Proceedings of the 8th Int’l symposium on leveraging applications of formal methods, verification and validation (ISoLA’18), LNCS. Springer
[105] Colombo, C.; Falcone, Y., Organising LTL monitors over distributed systems with a global clock, Formal Methods Syst Des, 49, 109-158 (2016) · Zbl 1380.68272
[106] Colombo C, Francalanza A, Mizzi R, Pace GJ (2012) polyLarva: Runtime verification with configurable resource-aware monitoring boundaries. In: Proceedings of the 10th Int’l conference on software engineering and formal methods (SEFM’12), volume 7504 of LNCS. Springer, pp 218-232
[107] Colombo, C.; Pace, GJ, Monitor-oriented compensation programming through compensating automata, ECEASST, 58, 1-12 (2013)
[108] Colombo, C.; Pace, GJ, Recovery within long running transactions, ACM Comput Surv, 45, 28 (2013) · Zbl 1293.68063
[109] Colombo, C.; Pace, GJ; Abela, P., Safer asynchronous runtime monitoring using compensations, Formal Methods Syst Des, 41, 269-294 (2012) · Zbl 1284.68142
[110] Cooper R, Marzullo K (1991) Consistent detection of global predicates. In: Proceedings of the ACM/ONR Workshop on parallel and distributed debugging (PADD ’91). ACM, pp 163-173
[111] Cormode G (2011) Continuous distributed monitoring: a short survey. In: Proceedings of the First Int’l workshop on algorithms and models for distributed event processing (AlMoDEP’11), volume 585 of ACM international conference proceeding series. ACM, New York, NY, USA, pp 1-10
[112] Cormode G, Garofalakis M (2005) Sketching streams through the net: distributed approximate query tracking. In: Proceedings of the 31st Int’l conference on very large data bases (VLDB’05). VLDB Endowment, pp 13-24
[113] Cormode, G.; Garofalakis, M.; Haas, PJ; Jermaine, C., Synopses for massive data: samples, histograms, wavelets, sketches, Found Trends Databases, 4, 1-294 (2012) · Zbl 1257.68062
[114] Cormode G, Garofalakis M, Muthukrishnan S, Rastogi R (2005) Holistic aggregates in a networked world: Distributed tracking of approximate quantiles. In: Proceedings of the 2005 ACM SIGMOD Int’l conference on management of data (SIGMOD’05). ACM, New York, NY, USA, pp 25-36
[115] Cormode, G.; Muthukrishnan, S.; Yi, K., Algorithms for distributed functional monitoring, ACM Trans Algorithms, 7, 21:1-21:20 (2011) · Zbl 1295.68204
[116] Cormode, G.; Muthukrishnan, S.; Yi, K.; Zhang, Q., Continuous sampling from distributed streams, J ACM, 59, 10:1-10:25 (2012) · Zbl 1281.68094
[117] Coulouris G (2011) Distributed systems: concepts and design. Addison-Wesley, Boston · Zbl 0708.68006
[118] Council of European Union. Regulation (EU) 2016/679 of the European Parliament and of the Council. http://eur-lex.europa.eu/legal-content/en/ALL/?uri=CELEX:32016R0679
[119] Dang T, Donzé A, Maler O (2004) Verification of analog and mixed-signal circuits using hybrid system techniques. In: Proceedings of the 5th Int’l conference on formal methods in computer-aided design (FMCAD’04), volume 3312 of LNCS. Springer, pp 21-36 · Zbl 1117.68303
[120] Dang T, Le Guernic C, Maler O (2009) Computing reachable states for nonlinear biological models. In: Proceedings of the 7th Int’l conference on computational methods in systems biology (CMSB’09), volume 5688 of LNCS. Springer, pp 126-141 · Zbl 1211.92023
[121] D’Angelo B, Sankaranarayanan S, Sánchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) LOLA: Runtime monitoring of synchronous systems. In: Proceedings of the 12th Int’l symposium of temporal representation and reasoning (TIME’05). IEEE CS Press, pp 166-174
[122] Demaine ED, López-Ortiz A, Munro JI (2002) Frequency estimation of Internet packet streams with limited space. In: Proceedings of the 10th annual European symposium on algorithms (ESA’02), volume 2461 of LNCS. Springer, pp 348-360 · Zbl 1019.68502
[123] Denning, DER, A lattice model of secure information flow, Commun ACM, 19, 236-243 (1976) · Zbl 0322.68034
[124] Denning, DER; Denning, PJ, Certification of programs for secure information flow, Commun ACM, 20, 504-513 (1977) · Zbl 0361.68033
[125] DEON conferences. https://deon2018.sites.uu.nl/
[126] Deshmukh, JV; Donzé, A.; Ghosh, S.; Jin, X.; Garvit, J.; Seshia, SA, Robust online monitoring of signal temporal logic, Formal Methods System Des, 51, 5-30 (2017) · Zbl 1370.68199
[127] Devriese D, Piessens F (2010) Noninterference through secure multi-execution. In: Proceedings of the 31st IEEE symposium on security and privacy (SP’10). IEEE, pp 109-124
[128] Dias RJ, Pessanha V, Lourenço JM (2013) Precise detection of atomicity violations. In: Hardware and software: verification and testing, volume 7857 of LNCS. Springer, pp 8-23 (HVC 2012 Best Paper Award)
[129] Distefano RJDD, Seco JC, Lourenço JM (2012) Verification of snapshot isolation in transactional memory Java programs. In: Noble J (ed) Proceedings of the 26th European conference on object-oriented programming (ECOOP’12), volume 7313 of LNCS. Springer, pp 640-664
[130] Dokhanchi A, Hoxha B, Fainekos GE (2014) On-line monitoring for temporal logic robustness. In Proceedings of the 5th Int’l conference on runtime verification (RV’14), LNCS. Springer, pp 231-246
[131] Donzé A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proceedings of the 22nd Int’l conference on computer aided verification (CAV’10), volume 6174 of LNCS. Springer, pp 167-170
[132] Donzé A, Ferrère T, Maler O (2013) Efficient robust monitoring for STL. In: Proceedings of the 25th Int’l conference on computer aided verification (CAV’13), volume 8044 of LNCS. Springer, pp 264-279
[133] Donzé A, Krogh B, Rajhans A (2009) Parameter synthesis for hybrid systems with an application to Simulink models. In: Proceedings of the 12th Int’l conference on hybrid systems: computation and control (HSCC’09), volume 5469 of LNCS. Springer, pp 165-179 · Zbl 1237.93089
[134] Donzé A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals. In: Proceedings of the 8th Int’l conference on formal modeling and analysis of timed systems (FORMATS’10), volume 6246 of LNCS. Springer, pp 92-106 · Zbl 1290.68071
[135] Donzé A, Maler O, Bartocci E, Ničković D, Grosu R, Smolka SA (2012) On temporal logic and signal processing. In: Proceedings of the 10th Int’l symposium on automated technology for verification and analysis (ATVA’12), volume 7561 of LNCS. Springer, pp 92-106 · Zbl 1374.68278
[136] Eisner C, Fisman D (2006) A practical introduction to PSL. Series on integrated circuits and systems. Springer, Berlin
[137] El-Hokayem A, Falcone Y (2017) Monitoring decentralized specifications. In: Proceedings of the 26th ACM SIGSOFT Int’l symposium on software testing and analysis (ISSTA’17). ACM, pp 125-135
[138] El-Hokayem A, Falcone Y (2018) On the monitoring of decentralized specifications semantics, properties, analysis, and simulation. CoRR. arXiv:1808.02692
[139] Ellul J, Pace GJ (2018) Runtime verification of Ethereum smart contracts. In: Proceedings of the 1st Int’l workshop on blockchain dependability, in conjunction with EDCC’18. IEEE
[140] Elnikety S, Zwaenepoel W, Pedone F (2005) Database replication using generalized snapshot isolation. In: Proceedings of the 24th IEEE symposium on reliable distributed systems (SRDS’05). IEEE Computer Society, pp 73-84
[141] Fagin R, Halpern JY, Moses Y, Vardi MY (2003) Reasoning about knowledge, vol 4. MIT press, Cambridge · Zbl 0839.68095
[142] Fainekos, GE; Giannakoglou, KC, Inverse design of airfoils based on a novel formulation of the ant colony optimization method, Inverse Probl Eng, 11, 21-38 (2003)
[143] Fainekos GE, Girard A, Pappas GJ (2006) Temporal logic verification using simulation. In: Proceedings of the 4th Int’l conference on formal modelling and analysis of timed systems (FORMATS’06), volume 4202 of LNCS. Springer, pp 171-186 · Zbl 1141.68463
[144] Fainekos, GE; Pappas, GJ, Robustness of temporal logic specifications for continuous-time signals, Theor Comput Sci, 410, 4279-4291 (2009) · Zbl 1186.68287
[145] Falcone Y, Cornebize T, Fernandez J (2014) Efficient and generalized decentralized monitoring of regular languages. In: Proceedings of 34th IFIP Int’l conference on formal techniques for distributed objects, components, and systems (FORTE’14), volume 8461 of LNCS. Springer, pp 66-83
[146] Falcone Y, Fernandez J, Mounier L (2009) Runtime verification of safety-progress properties. In: Bensalem S, Peled DA (eds) Runtime verification, 9th international workshop, RV 2009, Grenoble, France, June 26-28, 2009. Selected Papers, volume 5779 of Lecture Notes in Computer Science. Springer, pp 40-59
[147] Falcone, Y.; Fernandez, J.; Mounier, L., What can you verify and enforce at runtime?, Int J Softw Tools Technol Transf (STTT), 14, 349-382 (2012)
[148] Falcone, Y.; Jaber, M.; Nguyen, T-H; Bozga, M.; Bensalem, S., Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation, Softw Syst Model, 14, 173-199 (2015)
[149] Faymonville, Peter; Zimmermann, Martin, Parametric Linear Dynamic Logic, Electronic Proceedings in Theoretical Computer Science, 161, 60-73 (2014) · Zbl 1362.68169
[150] Feng S, Lohrey M, Quaas K (2015) Path checking for MTL and TPTL over data words. In: Potapov I (ed) Proceedings of the 19th Int’l conference on developments in language theory (DLT’15), volume 9168 of LNCS. Springer, pp 326-339 · Zbl 1434.68297
[151] Ferrère T, Maler O, Nickovic D (2015) Trace diagnostics using temporal implicants. In: Proceedings of the 13th International symposium on automated technology for verification and analysis (ATVA’15), volume 9364 of LNCS. Springer, pp 241-258 · Zbl 1471.68141
[152] Ferrère T, Maler O, Ničković D, Ulus D (2015) Measuring with timed patterns. In: Proceedings of the 27th Int’l conference on computer aided verification (CAV’15), volume 9207 of LNCS. Springer, pp 322-337 · Zbl 1381.68160
[153] Flajolet P, Fusy E, Gandouet O, Meunier F (2007) Hyperloglog: the analysis of a near-optimal cardinality estimation algorithm. In: Proceedings of the 2007 Int’l conference on analysis of algorithms (AOFA’07). DMTCS · Zbl 1192.68959
[154] Fraigniaud P, Rajsbaum S, Travers C (2014) On the number of opinions needed for fault-tolerant run-time monitoring in distributed systems. In: Proceedings of the 5th Int’l conference on runtime verification (RV’14), volume 8734 of LNCS. Springer, pp 92-107 · Zbl 1435.68196
[155] Francalanza A (2016) A theory of monitors—(extended abstract). In: Proceedings of the 19th Int’l conference on foundations of software science and computation structures (FOSSACS’16), volume 9634 of LNCS. Springer, pp 145-161 · Zbl 1476.68172
[156] Francalanza A (2017) Consistently-detecting monitors. In: Meyer R, Nestmann U (eds) Proceedings of the 28th Int’l conference on concurrency theory (CONCUR’17), volume 85 of Leibniz international proceedings in informatics (LIPIcs). Dagstuhl, Germany, pp 8:1-8:19. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik · Zbl 1442.68107
[157] Francalanza, A.; Aceto, L.; Ingolfsdottir, A., Monitorability for the Hennessy-Milner logic with recursion, Formal Methods Syst Des, 51, 87-116 (2017) · Zbl 1370.68203
[158] Francalanza, A.; Gauci, A.; Pace, GJ, Distributed system contract monitoring, J Log Algebraic Program, 82, 186-215 (2013) · Zbl 1283.68243
[159] Francalanza, A.; Hennessy, M., A theory for observational fault tolerance, J Log Algebraic Programm, 73, 22-50 (2007) · Zbl 1123.68080
[160] Francalanza, A.; Hennessy, M., A theory of system behaviour in the presence of node and link failure, Inf Comput, 206, 711-759 (2008) · Zbl 1152.68037
[161] Francalanza A, Mezzina CA, Tuosto E (2018) Reversible choreographies via monitoring in erlang. In: Proceedings of the 18th IFIP WG 6.1 Int’l conference on distributed applications and interoperable systems (DAIS’18), volume 10853 of LNCS. Springer, pp 75-92
[162] Francalanza A, Pérez JA, Sánchez C (2018) Runtime verification for decentralised and distributed systems. In: Bartocci E, Falcone Y (eds) Lectures on runtime verification—introductory and advanced topics, vol 10457. lecture notes in computer science. Springer, pp 176-210
[163] Francalanza, A.; Seychell, A., Synthesising correct concurrent runtime monitors, Formal Methods Syst Des, 46, 226-261 (2015) · Zbl 1323.68373
[164] Fränzle, M.; Herde, C.; Teige, T.; Ratschan, S.; Schubert, T., Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure, J Satisf Boolean Model Comput, 1, 209-236 (2007) · Zbl 1144.68371
[165] Frehse, G., PHAVer: algorithmic verification of hybrid systems past HyTech, Int J Softw Tools Technol Transfer, 10, 263-279 (2008) · Zbl 1078.93533
[166] Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: Scalable verification of hybrid systems. In: Proceedings of the 23rd Int’l conference on computer aided verification (CAV’11), volume 6806 of LNCS. Springer, pp 379-395
[167] Fuchs, NE, Specifications are (preferably) executable, Softw Eng J, 7, 323-334 (1992)
[168] Gait, J., A probe effect in concurrent programs, Softw Pract Exp, 16, 225-233 (1986)
[169] Gandon F, Governatori G, Villata S (2017) Normative requirements as linked data. In: Proceedings of the 30th annual conference on legal knowledge and information systems (JURIX’17), volume 302 of Frontiers in artificial intelligence and applications. IOS Press, pp 1-10
[170] Garcia R, Rodrigues R, Preguiça N (2011) Efficient middleware for byzantine fault tolerant database replication. In: Proceedings of the 6th conference on computer systems (EuroSys’11). ACM, pp 107-122
[171] García-Bañuelos L, Ponomarev A, Dumas M, Weber I (2017) Optimized execution of business processes on Blockchain. In: Proceedings of the 15th Int’l conference on business process management (BPM’17), volume 10445 of LNCS. Springer, pp 130-146
[172] Garg D, Jia L, Datta A (2011) Policy auditing over incomplete logs: theory, implementation and applications. In: Chen Y, Danezis G, Shmatikov V (eds) Proceedings of the 18th ACM conference on computer and communications security, (CCS’11). ACM, pp 151-162
[173] Garg VK (2002) Elements of distributed computing. Wiley-IEEE Press, Amsterdam
[174] Giacomo GD, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the 23rd Int’l joint conference on artificial intelligence (IJCAI’13). IJCAI/AAAI, pp 854-860
[175] Gilbertson S (2011) https://www.wired.com/2011/04/lessons-amazon-cloud-failure/
[176] Goguen JA, Meseguer J (1982) Security policies and security models. In: IEEE symposium on security and privacy. pp 11-20
[177] Goldreich O (ed) (2010) Property testing-current research and surveys, volume 6390 of LNCS. Springer, Berlin · Zbl 1197.68012
[178] Gouveia I, Rufino J (2016) Enforcing safety and security through non-intrusive runtime verification. In: Proceedings 1st workshop on security and dependability of critical embedded real-time systems. IEEE, Porto, pp 19-24
[179] Governatori, Guido; Rotolo, Antonino, Norm Compliance in Business Process Modeling, 194-209 (2010), Berlin, Heidelberg · Zbl 1197.68071
[180] Grigore R, Kiefer S (2018) Selective monitoring. In: Proceedings 29th Int’l conference on concurrency theory (CONCUR’18), volume 118 of LIPIcs. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, pp 20:1-20:16 · Zbl 1520.68101
[181] Gupta S, Krogh BH, Rutenbar RA (2004) Towards formal verification of analog designs. In: Proceedings of the Int’l conference on computer-aided design (ICCAD’04). IEEE CS Press, pp 210-217
[182] Gyllstrom D, Wu E, Chae H-J, Diao Y, Stahlberg P, Anderson G (2006) SASE: Complex event processing over streams. CoRR. arXiv:cs/0612128
[183] Haghighi I, Jones A, Kong Z, Bartocci E, Grosu R, Belta C (2015) SpaTeL: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th Int’l conference on hybrid systems: computation and control (HSCC’15). IEEE, pp 189-198 · Zbl 1366.68170
[184] Hallé, S.; Soucy-Boivin, M., MapReduce for parallel trace validation of LTL properties, J Cloud Comput, 4, 8 (2015)
[185] Havelund K, Goldberg A (2005) Verify your runs. In: Proceedings of the first IFIP TC 2/WG 2.3 Conference on verified software: theories, tools, experiments (VSTTE’05), volume 4171 of LNCS. Springer, pp 374-383
[186] Hayes, I.; Jones, CB, Specifications are not (necessarily) executable, Softw Eng J, 4, 330-338 (1989)
[187] Hedin D, Bello L, Sabelfeld A (2015) Value-sensitive hybrid information flow control for a Javascript-like language. In: Proceedings of the IEEE 28th computer security foundations symposium (CSF’15). IEEE, pp 351-365
[188] Hedin D, Sabelfeld A (2012) A perspective on information-flow control. In: Software safety and security, volume 33 of NATO science for peace and security series D: information and communication security. IOS Press, pp 319-347
[189] Henzinger TA, Kopke PW, Puri A, Varaiya P (1995) What’s decidable about hybrid automata?. ACM Press, New York, pp 373-382 · Zbl 0978.68534
[190] Herlihy M, Luchangco V, Moir M, Scherer III WN (2003) Software transactional memory for dynamic-sized data structures. In: Proceedings of the 22nd ACM symposium on principles of distributed computing (PODC’03). ACM, pp 92-101
[191] Herlihy, M.; Moss, JEB, Transactional memory: architectural support for lock-free data structures, SIGARCH Comput Arch News, 21, 289-300 (1993)
[192] Heule S, Rifkin D, Russo A, Stefan D (2015) The most dangerous code in the browser. In: 15th workshop on hot topics in operating systems (HotOS XV), Kartause Ittingen, Switzerland, 2015. USENIX Association
[193] Hunt S, Sands D (2006) On flow-sensitive security types. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL’06). ACM, pp 79-90 · Zbl 1370.68053
[194] IEEE (2012) IEEE P1800/D6, IEEE approved draft standard for system verilog—unified hardware design, specification, and verification language
[195] IEEE Standards Association (2012) IEC 62531, IEEE Std 1850 Standard for property specification language (PSL)
[196] Intel Corporation (2016) Control-flow enforcement technology preview
[197] Jacob, G.; Debar, H.; Filiol, E., Behavioral detection of malware: from a survey towards an established taxonomy, J Comput Virol, 4, 251-266 (2008)
[198] Journal of artificial intelligence and law. https://link.springer.com/journal/10506
[199] Jaksic S, Bartocci E, Grosu R, Kloibhofer R, Nguyen T, Ničković D (2015) From signal temporal logic to FPGA monitors. In: Proceedings of the the 13th ACM/IEEE international conference on formal methods and models for codesign (MEMOCODE’15). IEEE, pp 218-227
[200] Jaksic S, Bartocci E, Grosu R, Nickovic D (2016) Quantitative monitoring of STL with edit distance. In: Proceedings of the 16th Int’l conference on runtime verification (RV’16), volume 10012 of LNCS. Springer, pp 201-218 · Zbl 1394.68230
[201] Jaksic, S.; Bartocci, E.; Grosu, R.; Nickovic, D., An algebraic framework for runtime verification, IEEE Trans CAD Integr Circuits Syst, 37, 2233-2243 (2018)
[202] Joyce, J.; Lomow, G.; Slind, K.; Unger, B., Monitoring distributed systems, ACM Trans Comput Syst, 5, 121-150 (1987)
[203] Joyce, J.; Lomow, G.; Slind, K.; Unger, BW, Monitoring distributed systems, ACM Trans Comput Syst, 5, 121-150 (1987)
[204] JURIX conferences. http://jurix.nl
[205] Kalajdzic K, Bartocci E, Smolka SA, Stoller SD, Grosu R (2013) Runtime verification with particle filtering. In: Proceedings of the 4th Int’l conference on runtime verification (RV’13), volume 8174 of LNCS. Springer, pp 149-166
[206] Kane A (2015) Runtime monitoring for safety-critical embedded systems. PhD thesis, Carnegie Mellon University, USA
[207] Kane A, Chowdhury O, Datta A, Koopman P (2015) A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Proceedings of the 15th international conference on runtime verification (RV’15), volume 9333 of LNCS. Springer, pp 102-117
[208] Karp, RM; Shenker, S.; Papadimitriou, CH, A simple algorithm for finding frequent elements in streams and bags, ACM Trans Database Syst, 28, 51-55 (2003)
[209] Kenny JR, Mackin B (2007) FPGA coprocessing in multi-core architectures for DSP. Altera Corporation Application Note
[210] Keralapura R, Cormode G, Ramamirtham J (2006) Communication-efficient distributed monitoring of thresholded counts. In: Proceedings of the 2006 ACM SIGMOD Int’l conference on management of data (SIGMOD’06). ACM, pp 289-300
[211] KeY (2017) https://www.key-project.org/applications/program-verification
[212] Kim ES, Sadraddini S, Belta C, Arcak M, Seshia SA (2017) Dynamic contracts for distributed temporal logic control of traffic networks. In: Prceedings of the IEEE 56th annual conference on decision and control (CDC’17). IEEE, pp 3640-3645
[213] Kong S, Gao S, Chen W, Clarke E (2015) dReach: \( \delta \)-reachability analysis for hybrid systems. In: Proceedings of the 21st Int’l conference on tools and algorithms for the construction and analysis of systems (TACAS’15), volume 9035 of LNCS. Springer, pp 200-205
[214] Koymans, R., Specifying real-time properties with metric temporal logic, Real Time Syst, 2, 255-299 (1990)
[215] Kuhn, T., A survey and classification of controlled natural languages, J Comput Linguist, 40, 121-170 (2014)
[216] Kuhtz L, Finkbeiner B (2009) LTL path checking is efficiently parallelizable. In: Proceedings of the 36th Int’l colloquium on automata, languages and programming (ICALP’09): Part II, volume 5556 of LNCS. Springer, pp 235-246 · Zbl 1248.68252
[217] Kuhtz, L.; Finkbeiner, B., Efficient parallel path checking for linear-time temporal logic with past and bounds, Log Methods Comput Sci, 8, 1-24 (2012) · Zbl 1253.68221
[218] Lamport, L., Time, clocks, and the ordering of events in a distributed system, Commun ACM, 21, 558-565 (1978) · Zbl 0378.68027
[219] Lamport, L., The part-time parliament, ACM Trans Comput Syst, 16, 133-169 (1998)
[220] Le Guernic G, Banerjee A, Jensen TP, Schmidt DA (2006) Automata-based confidentiality monitoring. In: Proceedings of the 11th Asian computing science conference—secure software and related issues (ASIAN’06), volume 4435 of LNCS. Springer
[221] Lee JC, Gardnerd AS, Lysecky R (2011) Hardware observability framework for minimally intrusive online monitoring of embedded systems. Proceedings 18th international conference on engineering of computer based systems (ECBS’11). IEEE Computer Sociery, Las Vegas, USA, pp 52-60
[222] Lee, JC; Lysecky, R., System-level observation framework for non-intrusive runtime monitoring of embedded systems, ACM Trans Des Autom Electron Syst, 20, 42:1-42:27 (2015)
[223] Lessig L (1999) Code and other laws of cyberspace. Basic Books, New York
[224] Leucker M, Sánchez C (2007) Regular linear temporal logic. In: Proceedings of The 4th Int’l colloquium on theoretical aspects of computing (ICTAC’07), volume 4711 of LNCS. Springer, pp 291-305 · Zbl 1147.03305
[225] Leucker, M.; Schallhart, C., A brief account of runtime verification, J Logi Algebraic Program, 78, 293-303 (2009) · Zbl 1192.68433
[226] Liskov B, Ghemawat S, Gruber R, Johnson P, Shrira L, Williams M (1991) Replication in the harp file system. In: Proceedings of the 13th ACM symposium on operating systems principles (SOSP’91). ACM, pp 226-238
[227] Lomet, DB, Process structuring, synchronization, and recovery using atomic actions, SIGSOFT Softw Eng Notes, 2, 128-137 (1977)
[228] Lomuscio, A.; Sergot, MJ, Deontic interpreted systems, Studia Logica, 75, 63-92 (2003) · Zbl 1033.03012
[229] Loreti D, Chesani F, Ciampolini A, Mello P (2017) Distributed compliance monitoring of business processes over MapReduce architectures. In: Proceedings of the 8th ACM/SPEC Int’l conference on performance engineering companion (ICPE’17). ACM, pp 79-84
[230] Lourenço JM, Dias RJ, Luís J, Rebelo M, Pessanha V (2009) Understanding the behavior of transactional memory applications. In: Proceedings of the 7th workshop on parallel and distributed systems: testing, analysis, and debugging (PADTAD’09). ACM, Chicago, Illinois, pp 31-39
[231] Luckham DC (2005) The power of events-an introduction to complex event processing in distributed enterprise systems. ACM, New York
[232] Lundqvist T, Stenstrom P (1999) Timing anomalies in dynamically scheduled microprocessors. In: Proceedings of the 20th IEEE real-time systems symposium (RTSS’99). IEEE Computer Society
[233] Luo Q, Roşu G (2013) EnforceMOP: A runtime property enforcement system for multithreaded programs. In: Proceedings of the 2013 Int’l symposium on software testing and analysis (ISSTA’13). ACM, pp 156-166
[234] Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Proceedings of the joint Int’l conferences on formal modelling and analysis of timed systems (FORMATS’04) and formal techniques in real-time and fault-tolerant systems (FTRTFT’04), volume 3253 of LNCS. Springer, pp 152-166 · Zbl 1109.68518
[235] Maler, O.; Nickovic, D., Monitoring properties of analog and mixed-signal circuits, STTT, 15, 247-268 (2013)
[236] Manjhi A, Shkapenyuk V, Dhamdhere K, Olston C (2005) Finding (recently) frequent items in distributed data streams. In: Proceedings of the 21st Int’l conference on data engineering (ICDE’05). IEEE Computer Society, Washington, DC, USA, pp 767-778
[237] Margara A, Cugola G (2011) Processing flows of information: from data stream to complex event processing. In: Proceedings of the 5th ACM Int’l conference on distributed event-based systems (DEBS’11). ACM, pp 359-360
[238] Meyer B (1992) Eiffel: the language. Prentice Hall, Upper Saddle River · Zbl 0779.68013
[239] Mims C (2017) All IT jobs are cybersecurity jobs now. Wall Street J. https://www.wsj.com/articles/all-it-jobs-are-cybersecurity-jobs-now-1495364418
[240] Misra, J.; Gries, D., Finding repeated elements, Sci Comput Program, 2, 143-152 (1982) · Zbl 0497.68041
[241] Mittal, N.; Sen, A.; Garg, VK, Solving computation slicing using predicate detection, IEEE Trans Parallel Distrib Syst (TPDS), 18, 1700-1713 (2007)
[242] Molina-Jiménez C, Shrivastava SK (2013) Establishing conformance between contracts and choreographies. In: Proceedings of the IEEE 15th conference on business informatics (CBI’13). IEEE Computer Society, pp 69-78
[243] Morris, R., Counting large numbers of events in small registers, Commun ACM, 21, 840-842 (1978) · Zbl 0386.68035
[244] Mozafari B (2017) Approximate query engines: commercial challenges and research opportunities. In: Proceedings of the 2017 ACM Int’l conference on management of data (SIGMOD’17). ACM, pp 521-524
[245] Mozafari B, Ramnarayan J, Menon S, Mahajan Y, Chakraborty S, Bhanawat H, Bachhav K (2017) Snappydata: a unified cluster for streaming, transactions and interactice analytics. In: Proceedings of the 8th biennial conference on innovative data systems research (CIDR’17)
[246] Murray DG, McSherry F, Isaacs R, Isard M, Barham P, Abadi M (2013) Naiad: a timely dataflow system. In: ACM SIGOPS 24th symposium on operating systems principles, SOSP ’13, Farmington, PA, USA, November 3-6, 2013. pp 439-455
[247] Nakamoto S (2008) Bitcoin: A peer-to-peer electronic cash system. Bitcoin.org
[248] Nam TH (2017) Cache memory aware priority assignment and scheduling simulation of real-time embedded systems. PhD thesis, Université de Bretagne Occidentale, Brest, France
[249] Nazarpour, H.; Falcone, Y.; Bensalem, S.; Bozga, M., Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation, Formal Asp Comput, 29, 951-986 (2017) · Zbl 1377.68042
[250] Nelson, J., Sketching and streaming algorithms for processing massive data, ACM Crossroads, 19, 14-19 (2012)
[251] Nenzi L, Bortolussi L, Ciancia V, Loreti M, Massink M (2015) Qualitative and quantitative monitoring of spatio-temporal properties. In: Proceedings of the 6th Int’l conference on runtime verification (RV’15), volume 9333 of LNCS. Springer, pp 21-37 · Zbl 1448.68313
[252] Nghiem T, Sankaranarayanan S, Fainekos GE, Ivancic F, Gupta A, Pappas GJ (2010) Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of the 13th ACM Int’l conference on hybrid systems: computation and control (HSCC’10). ACM, pp 211-220 · Zbl 1361.68149
[253] Nguyen T, Bartocci E, Ničković D, Grosu R, Jaksic S, Selyunin K (2016) The HARMONIA project: hardware monitoring for automotive systems-of-systems. In: Proceedings of 7th Int’l symposium on leveraging applications of formal methods, verification and validation (ISoLA’16), volume 9953 of LNCS. Springer, pp 371-379
[254] Nickovic D, Lebeltel O, Maler O, Ferrere T (2018) AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. In: Proceedings of the Int’l conference on tools and algorithms for the construction and analysis of systems (TACAS’18), volume 10806 of LNCS. Springer, pp 303-319
[255] Orme W (2008) Debug and trace for multicore SoCs: How to build an efficient and effective debug and trace system for complex, multicore SoCs. ARM White paper
[256] Orosa L, Lourenço JM (2016) A hardware approach for detecting, exposing and tolerating high level atomicity violations. In: Proceedings of the 24th Euromicro Int’l conference on parallel, distributed, and network-based processing (PDP’16). IEEE Computer Society, pp 159-167
[257] Pace GJ, Schneider G (2009) Challenges in the specification of full contracts. In: Proceedings of the 7th Int’l conference on integrated formal methods (iFM’09), volume 5423 of LNCS. Springer, pp 292-306 · Zbl 1211.68251
[258] Pant YV, Abbas H, Mangharam R (2017) Smooth operator: control using the smooth robustness of temporal logic. In: Proceedings of the 2017 IEEE conference on control technology and applications (CCTA’17). IEEE, pp 1235-1240
[259] Pardo R, Colombo C, Pace G, Schneider G (2016) An automata-based approach to evolving privacy policies for social networks. In: Proceedings of the 16th Int’l conference on runtime verification (RV’16), volume 10012 of LNCS. Springer, pp 285-301
[260] Pardo R, Kellyérová I, Sánchez C, Schneider G (2016) Specification of evolving privacy policies for online social networks. In: Proceedings of the 23rd international symposium on temporal representation and reasoning (TIME’16). IEEE Computer Society, pp 70-79
[261] Pardo R, Sánchez C, Schneider G (2018) Timed epistemic knowledge bases for social networks. In: Proceedings of the 22nd Int’l symposium on formal methods (FM’18), volume 10951 of LNCS. Springer, pp 185-202 · Zbl 1460.68101
[262] Pardo R, Schneider G (2014) A formal privacy policy framework for social networks. In: 12th International conference on software engineering and formal methods (SEFM’14), volume 8702 of LNCS. Springer, pp 378-392
[263] Passmore GO, Ignatovich D (2017) Formal verification of financial algorithms. In: Proceedings of the 26th Int’l conference on automated deduction (CADE’17), volume 10395 of LNCS. Springer, pp 26-41
[264] Patel P, Bansal D, Yuan L, Murthy A, Greenberg A, Maltz DA, Kern R, Kumar H, Zikos M, Wu H, Kim C, Karri N (2013) Ananta: cloud scale load balancing. In: Proceedings of the ACM SIGCOMM 2013 conference (SIGCOMM ’13), SIGCOMM ’13. ACM, pp 207-218
[265] Pellizzoni R, Meredith P, Caccamo M, Rosu G (2008) Hardware runtime monitoring for dependable COTS-based real-time embedded systems. In: Proceedings of the IEEE real-time systems symposium (RTSS’08). IEEE Computer Society, pp 481-491
[266] Phan LTX, Lee I, Sokolsky O (2011) A semantic framework for mode change protocols. In: Proceedings of the 17th IEEE real-time and embedded technology and applications symposium (RTAS’11). IEEE Computer Society, pp 91-100
[267] Picazo-Sánchez P, Schneider G, Tapiador J (2019) After you, please: browser extensions order attacks and countermeasures. CoRR - arXiv.org. https://arxiv.org/abs/1908.02205
[268] Pike L, Niller S, Wegmann N (2011) Runtime verification for ultra-critical systems. In: Proceedings of the 2nd Int’l conference on runtime verification (RV’11), volume 7186 of LNCS. Springer, pp 310-324
[269] Pinisetty S, Sands D, Schneider G (2018) Runtime verification of hyperproperties for deterministic programs. In: Proceedings of the 6th Int’l conference on formal methods in software engineering (FormaliSE’18). ACM
[270] Pinto RC, Rufino J (July 2014) Towards non-invasive runtime verification of real-time systems. In: Proceedings of the 26th Euromicro conference on real-time systems—WIP session. Euromicro, pp 25-28
[271] Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: Proceedings of the 14th Int’l symposium on formal methods (FM’06), volume 4085 of LNCS. Springer, pp 573-586
[272] Prakken H, Sartor G (2013) Formalising arguments about norms. In: Proceedings of the 26th annual conference on legal knowledge and information systems (JURIX’13), volume 259 of Frontiers in artificial intelligence and applications. IOS Press, pp 121-130
[273] Prisacariu, C.; Schneider, G., A dynamic deontic logic for complex contracts, J Log Algebraic Program, 81, 458-490 (2012) · Zbl 1258.03024
[274] Prybila C, Schulte S, Hochreiner C, Weber I (2017) Runtime verification for business processes utilizing the Bitcoin Blockchain. CoRR. arXiv:1706.04404
[275] Rahmatian M, Kooti H, Harris IG, Bozorgzadeh E (2012) Adaptable intrusion detection using partial runtime reconfiguration. In: Proceedings of the IEEE 30th Int’l conference on computer design (ICCD’12). IEEE Computer Society, pp 147-152
[276] Raman V, Donzé A, Maasoumy M, M RM, Sangiovanni-Vincentelli A, Seshia SA (2014) Model predictive control with signal temporal logic specifications. In: Proceedings of the 53rd annual conference on decision and control (CDC’14). IEEE, pp 81-87
[277] Raman V, Donzé A, Sadigh D, Murray RM, Seshia SA (2015) Reactive synthesis from signal temporal logic specifications. In: Proceedings HSCC’15: the 18th international conference on hybrid systems: computation and control. ACM, pp 239-248 · Zbl 1366.68180
[278] Ravichandran K, Gavrilovska A, Pande S (2014) DeSTM: harnessing determinism in STMs for application development. In: Proceedings of the Int’l conference on parallel architectures and compilation (PACT). ACM, pp 213-224
[279] Reger G, Rydeheard D (2015) From first-order temporal logic to parametric trace slicing. In: Proceedings of the 6th Int’l conference on runtime verification (RV’15), LNCS. Springer, pp 216-232
[280] Reinbacher, T.; Fugger, M.; Brauer, J., Runtime verification of embedded real-time systems, Formal Methods Syst Des, 24, 203-239 (2014) · Zbl 1317.68122
[281] Reinbacher T, Rozier KY, Schumann J (2014) Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings 20th international conference on tools and algorithms for the construction and analysis of systems (TACAS’14), volume 8413 of LNCS. Springer, pp 357-372
[282] Reinders J (2013) Intel processor tracing. Intel Corporation, Santa Clara
[283] Reliable smart contracts: State-of-the-art, applications, challenges and future directions. http://www.isp.uni-luebeck.de/Isola2018-SmartContracts. ISoLA’18 track (http://www.isola-conference.org/isola2018/tracks.html)
[284] Rizk A, Batt G, Fages F, Soliman S (2008) On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Proceedings of the 6th Int’l conference on computational methods in systems biology (CMSB’08), volume 5307 of LNCS. Springer, pp 251-268
[285] Rodionova A, Bartocci E, Ničković D, Grosu R (2016) Temporal logic as filtering. In: Proceedings of HSCC 2016: the 19th International conference on hybrid systems: computation and control. ACM, pp 11-20 · Zbl 1364.94156
[286] Rufino, J., Towards integration of adaptability and non-intrusive runtime verification in avionic systems, ACM SIGBED Rev, 13, 60-65 (2016)
[287] Rufino J, Gouveia I (July 2016) Timeliness runtime verification and adaptation in avionic systems. In: Proceedings of the 12th workshop on operating systems platforms for embedded real-time applications (OSPERT’16). Euromicro, Toulouse, France, pp 14-20
[288] RuleML conferences. http://2018.ruleml-rr.org
[289] Russo A, Sabelfeld A (2010) Dynamic vs. static flow-sensitive security analysis. In: Proceedings of the 23rd IEEE computer security foundations symposium (CSF’10). IEEE Computer Society, pp 186-199
[290] Sabelfeld, A.; Myers, AC, Language-based information-flow security, J Sel Areas Commun, 21, 5-19 (2003)
[291] Saini, A.; Gaur, MS; Laxmi, V.; Conti, M., Colluding browser extension attack on user privacy and its implication for web browsers, Comput Secur, 63, 14-28 (2016)
[292] Salem MB, Hershkop S, Stolfo SJ (2008) A survey of insider attack detection research. In: Insider attack and cyber security—beyond the hacker. Springer, pp 69-90
[293] Sánchez C, Leucker M (2010) Regular linear temporal logic with past. In: Proceedings of the 11th Int’l conference on verification, model checking, and abstract interpretation, (VMCAI’10), volume 5944 of LNCS. Springer, pp 295-311 · Zbl 1273.03064
[294] Santos JF, Jensen T, Rezk T, Schmitt A (2015) Hybrid Typing of Secure Information Flow in a JavaScript-like Language. In: Proceedings of the 10th Int’l symposium on on trustworthy global computing (TGC’15), volume 9533 of LNCS. Springer
[295] Schneider, FB, Implementing fault-tolerant services using the state machine approach: a tutorial, ACM Comput Surv, 22, 299-319 (1990)
[296] Schultz-Møller NP, Migliavacca M, Pietzuch P (2009) Distributed complex event processing with query rewriting. In: Proceedings of the 3rd ACM Int’l conference on distributed event-based systems (DEBS’09). ACM, pp 4:1-4:12
[297] Selyunin K, Jaksic S, Nguyen T, Reidl C, Hafner U, Bartocci E, Nickovic D, Grosu R (2017) Runtime monitoring with recovery of the SENT communication protocol. In: Proceedings of the the 29th Int’l conference on computer aided verification (CAV’17), volume 10426 of LNCS. Springer, pp 336-355
[298] Sen K, Vardhan A, Agha G, Rosu G (2004) Efficient decentralized monitoring of safety in distributed systems. In: Proceedings of 26th Int’l conference on software engineering (ICSE 2004). IEEE CS Press, pp 418-427
[299] Shabtai A, Elovici Y, Rokach L (2012) A survey of data leakage detection and prevention solutions. Springer briefs in computer science. Springer, Berlin
[300] Shekita, JREJ; Tata, S., Using Paxos to build a scalable, consistent, and highly available datastore, Proc VLDB Endow, 4, 243-254 (2011)
[301] Shobaki ME, Lindh L (2001) A hardware and software monitor for high-level system-on-chip verification. In: Proceedings of the 2nd IEEE Int’l symposium on quality electronic design (ISQED 2001). pp 56-61
[302] Spoth W, Arab BS, Chan ES, Dieter G, Ghoneimy A, Glavic B, Hammerschmidt B, Kennedy O, Lee S, Liu ZH, Niu X, Yang Y (2017) Adaptive schema databases. In: Proceedings of the 8th biennial Int’l on innovative data systems research (CIDR’17). CIDRDB
[303] Stoller SD, Bartocci E, Seyster J, Grosu R, Havelund K, Smolka SA, Zadok E (2011) Runtime verification with state estimation. In: Proceedings of the 2nd Int’l conference on runtime verification (RV’11), volume 7186 of LNCS. Springer, pp 193-207
[304] Suiche M (2017) WannaCry—the largest ransom-ware infection in history. https://blog.comae.io/wannacry-the-largest-ransom-ware-infection-in-history-f37da8e30a58
[305] Szabo N (1996) Smart contracts: building blocks for digital markets. Extropy 16
[306] Todman T, Stilkerich S, Luk W (2015) In-circuit temporal monitors for runtime verification of reconfigurable designs. In: Proceedings of the 52nd annual design automation conference (DAC’15). ACM, pp 50:1-50:6
[307] Tsankov P, Marinovic S, Dashti MT, Basin DA (2014) Decentralized composite access control. In: Abadi M, Kremer S (eds) Proceedings of the 3rd Int’l conference principles of security and trust (POST’14), volume 8414 of LNCS. Springer, pp 245-264
[308] Ulus D, Ferrère T, Asarin E, Maler O (2014) Timed pattern matching. In: Proceedings of the 12th Int’l conference on Formal modeling and analysis of timed systems (FORMATS’14), volume 8711 of LNCS. Springer, pp 222-236 · Zbl 1419.68221
[309] Ulus, Dogan; Ferrère, Thomas; Asarin, Eugene; Maler, Oded, Online Timed Pattern Matching Using Derivatives, 736-751 (2016), Berlin, Heidelberg · Zbl 1420.68247
[310] Vachharajani N, Bridges MJ, Chang J, Rangan R, Ottoni G, Blome JA, Reis GA, Vachharajani M, August DI (2004) Rifle: An architectural framework for user-centric information-flow security. In: Proceedings of the 37th Int’l symposium on microarchitecture (MICRO’04). IEEE Computer Society, pp 243-254
[311] Vale, TM; Silva, JA; Dias, RJ; Lourenço, JM, Pot: Deterministic transactional execution, ACM Trans Arch Code Optim, 13, 52:1-52:24 (2016)
[312] van der Aalst WMP (2012) Distributed process discovery and conformance checking. In Proceedings of the 15th Int’l conference on fundamental approaches to software engineering (FASE’12), volume 7212 of LNCS. Springer, Berlin, Heidelberg, pp 1-25
[313] Vardi MY (2008) From Church and Prior to PSL. In: 25 Years of model checking—history, achievements, perspectives, volume 5000 of LNCS. Springer, pp 150-171 · Zbl 1142.68051
[314] Viswanathan M (2000) Foundations for the run-time analysis of software systems. PhD thesis, University of Pennsylvania
[315] Volpano, D.; Irvine, C.; Smith, G., A sound type system for secure flow analysis, J Comput Secur, 4, 167-187 (1996)
[316] Watterson, C.; Heffernan, D., Runtime verification and monitoring of embedded systems, IET Softw, 1, 172-179 (2007)
[317] Weber I, Xu X, Riveret R, Governatori G, Ponomarev A, Mendling J (2016) Untrusted business process monitoring and execution using Blockchain. In: Proceedings of the 14th Int’l conference on business process management (BPM’16), volume 9850 of LNCS. Springer, pp 329-347
[318] Weil SA, Brandt SA, Miller EL, Long DDE, Maltzahn C (2006) Ceph: a scalable, high-performance distributed file system. In: Proceedings of the 7th symposium on operating systems design and implementation (OSDI’06), OSDI ’06. USENIX Association, pp 307-320
[319] White W, Riedewald M, Gehrke J, Demers A (2007) What is “next” in event processing?. In: Proceedings of the 26th ACM SIGMOD-SIGACT-SIGART symposium on principles of database systems (PODS’07). ACM, New York, NY, USA, pp 263-272
[320] Wilhelm, R.; Engblom, J.; Ermedahl, A.; Holsti, N.; Thesing, S.; Whalley, D.; Bernat, G.; Ferdinand, C.; Heckmann, R.; Mitra, T.; Mueller, F.; Puaut, I.; Puschner, P.; Staschulat, J.; Stenstrom, P., The worst-case execution time problem—overview of methods and survey of tools, ACM Trans Embed Comput Syst, 7, 36 (2008)
[321] Wongpiromsarn, T.; Topcu, U.; Murray, RM, Receding horizon temporal logic planning, IEEE Trans Autom Control, 57, 2817-2830 (2012) · Zbl 1369.93392
[322] Wood G (2014) Ethereum: A secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper 151:1-32
[323] Woodruff DP, Zhang Q (2012) Tight bounds for distributed functional monitoring. In: Proceedings of the 44th annual acm symposium on theory of computing (STOC’12). ACM, pp 941-960 · Zbl 1286.68025
[324] Wright, GHV, Deontic logic, Mind, 60, 1-15 (1951)
[325] WSLA. www.research.ibm.com/wsla/
[326] Wyner AZ (2015) From the language of legislation to executable logic programs. In: Logic in the theory and practice of lawmaking, volume 2 of legisprudence library. Springer, pp 409-434
[327] Wyner AZ, Angelov K, Barzdins G, Damljanovic D, Davis B, Fuchs NE, Höfler S, Jones K, Kaljurand K, Kuhn T (2009) On controlled natural languages: properties and prospects. In: CNL’09, volume 5972 of LNCS. Springer, pp 281-289
[328] Xiaoqing J, Donzé A, Deshmukh JV, Seshia SA (2013) Mining Requirements from closed-loop control models. In: Proceedings of the ACM international conference on hybrid systems: computation and control (HSCC’13). ACM, pp 43-52 · Zbl 1362.93008
[329] Xie C, Su C, Kapritsos M, Wang Y, Yaghmazadeh N, Alvisi L, Mahajan P (2014) Salt: combining ACID and BASE in a distributed database. In: Proceedings of the 11th USENIX conference on operating systems design and implementation (OSDI’14). USENIX Association, pp 495-509
[330] Xie C, Su C, Littley C, Alvisi L, Kapritsos M, Wang Y (2015) High-performance ACID via modular concurrency control. In: Proceedings of the 25th symposium on operating systems principles (SOSP’15). ACM, pp 279-294
[331] Yaghoubi S, Fainekos G (2017) Hybrid approximate gradient and stochastic descent for falsification of nonlinear systems. In: Proceedings the 2017 American control conference (ACC’17). IEEE, pp 529-534
[332] Yang H, Hoxha B, Fainekos G (2012) Querying parametric temporal logic properties on embedded systems. In: Proceedings of the 24th IFIP WG 6.1 Int’l conference on testing software and systems (ICTSS’12), volume 7641 of LNCS. Springer, pp 136-151
[333] Yang J, Hance T, Austin TH, Solar-Lezama A, Flanagan C, Chong S (June 2016) Precise, dynamic information flow for database-backed applications. In: Proceedings of the 37th ACM SIGPLAN conference on programming language design and implementation (PLDI’16). ACM, pp 631-647
[334] Ye, Y.; Li, T.; Adjeroh, D.; Iyengar, SS, A survey on malware detection using data mining techniques, ACM Comput Surv, 50, 41:1-41:40 (2017)
[335] Yi, K.; Zhang, Q., Optimal tracking of distributed heavy hitters and quantiles, Algorithmica, 65, 206-223 (2013) · Zbl 1259.68042
[336] Yu, B.; Duan, Z.; Tian, C.; Zhang, N., Verifying temporal properties of programs: a parallel approach, J Parallel Distrib Comput, 118, 89-99 (2017)
[337] Zaharia M, Chowdhury M, Franklin MJ, Shenker S, Stoica I (2010) Spark: Cluster computing with working sets. In: Proceedings of the 2nd USENIX Workshop on hot topics in cloud computing (HotCloud’10). USENIX Association
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.