Formal Methods in System DesignAn International Journal Short Title: Form. Methods Syst. Des. Publisher: Springer US, New York, NY ISSN: 0925-9856; 1572-8102/e Online: https://link.springer.com/journal/10703/volumes-and-issues Comments: Journal; Indexed cover-to-cover Documents Indexed: 562 Publications (since 1992) References Indexed: 448 Publications with 16,837 References. all top 5 Latest Issues 61, No. 2-3 (2022) 61, No. 1 (2022) 60, No. 3 (2022) 60, No. 2 (2022) 60, No. 1 (2022) 59, No. 1-3 (2021) 58, No. 3 (2021) 58, No. 1-2 (2021) 57, No. 3 (2021) 57, No. 2 (2021) 57, No. 1 (2021) 56, No. 1-3 (2020) 55, No. 3 (2020) 55, No. 2 (2019) 55, No. 1 (2019) 54, No. 3 (2019) 54, No. 2 (2019) 54, No. 1 (2019) 53, No. 3 (2018) 53, No. 2 (2018) 53, No. 1 (2018) 52, No. 3 (2018) 52, No. 2 (2018) 52, No. 1 (2018) 51, No. 3 (2017) 51, No. 2 (2017) 51, No. 1 (2017) 50, No. 2-3 (2017) 50, No. 1 (2017) 49, No. 3 (2016) 49, No. 1-2 (2016) 48, No. 3 (2016) 48, No. 1-2 (2016) 47, No. 3 (2015) 47, No. 2 (2015) 47, No. 1 (2015) 46, No. 3 (2015) 46, No. 2 (2015) 46, No. 1 (2015) 45, No. 3 (2014) 45, No. 2 (2014) 45, No. 1 (2014) 44, No. 3 (2014) 44, No. 2 (2014) 44, No. 1 (2014) 43, No. 3 (2013) 43, No. 2 (2013) 43, No. 1 (2013) 42, No. 3 (2013) 42, No. 2 (2013) 42, No. 1 (2013) 41, No. 3 (2012) 41, No. 2 (2012) 41, No. 1 (2012) 40, No. 3 (2012) 40, No. 2 (2012) 40, No. 1 (2012) 39, No. 3 (2011) 39, No. 2 (2011) 39, No. 1 (2011) 38, No. 3 (2011) 38, No. 2 (2011) 38, No. 1 (2011) 37, No. 2-3 (2010) 37, No. 1 (2010) 36, No. 3 (2010) 36, No. 2 (2010) 36, No. 1 (2010) 35, No. 3 (2009) 35, No. 2 (2009) 35, No. 1 (2009) 34, No. 3 (2009) 34, No. 2 (2009) 34, No. 1 (2009) 33, No. 1-3 (2008) 32, No. 3 (2008) 32, No. 2 (2008) 32, No. 1 (2008) 31, No. 3 (2007) 31, No. 2 (2007) 31, No. 1 (2007) 30, No. 3 (2007) 30, No. 2 (2007) 30, No. 1 (2007) 29, No. 3 (2006) 29, No. 2 (2006) 29, No. 1 (2006) 28, No. 3 (2006) 28, No. 2 (2006) 28, No. 1 (2006) 27, No. 3 (2005) 27, No. 1-2 (2005) 26, No. 3 (2005) 26, No. 2 (2005) 26, No. 1 (2005) 25, No. 2-3 (2004) 25, No. 1 (2004) 24, No. 3 (2004) 24, No. 2 (2004) 24, No. 1 (2004) ...and 30 more Volumes all top 5 Authors 12 Strichman, Ofer 12 Vardi, Moshe Ya’akov 11 Clarke, Edmund Melson jun. 11 Kröning, Daniel 9 Grumberg, Orna 9 Tonetta, Stefano 8 Falcone, Yliès 8 Peled, Doron A. 7 Alur, Rajeev 7 Barrett, Clark W. 7 Bloem, Roderick 7 Bouajjani, Ahmed 7 Chockler, Hana 7 Sharygina, Natasha 6 Biere, Armin 6 Chaki, Sagar 6 Cimatti, Alessandro 6 Havelund, Klaus 6 Henzinger, Thomas A. 6 Katoen, Joost-Pieter 6 Kupferman, Orna 6 Larsen, Kim Guldstrand 6 Raskin, Jean-François 6 Rümmer, Philipp 6 Weissenbacher, Georg 5 Chakraborty, Supratik 5 Chatterjee, Krishnendu 5 Dill, David L. 5 Esparza, Javier 5 Fribourg, Laurent 5 Gopalakrishnan, Ganesh Lalitha 5 Griggio, Alberto 5 Gurfinkel, Arie 5 Heyman, Tamir 5 Kwiatkowska, Marta Z. 5 Reynolds, Andrew 5 Tripakis, Stavros 5 Viswanathan, Mahesh 5 Vojnar, Tomáš 5 Yorav, Karen 4 Abdulla, Parosh Aziz 4 Baier, Christel 4 Bartocci, Ezio 4 Ben-David, Shoham 4 Cabodi, Gianpiero 4 Eisner, Cindy 4 Fisher, Michael 4 Grosu, Radu 4 Habermehl, Peter 4 Jéron, Thierry 4 McMillan, Kenneth L. 4 Mover, Sergio 4 Norman, Gethin 4 Păsăreanu, Corina S. 4 Platzer, André 4 Roşu, Grigore 4 Sánchez, César 4 Sangiovanni-Vincentelli, Alberto L. 4 Sankaranarayanan, Sriram 4 Seshia, Sanjit Arunkumar 4 Stoller, Scott D. 4 Tinelli, Cesare 3 Abraham, Jacob A. 3 Andersen, Henrik Reif 3 Aziz, Adnan 3 Basin, David A. 3 Becker, Bernd 3 Beer, Ilan 3 Benveniste, Albert 3 Bérard, Béatrice 3 Bonakdarpour, Borzoo 3 Bouyer, Patricia 3 Claesen, Luc 3 Colombo, Christian 3 Cook, Byron 3 Damm, Werner 3 Dixon, Clare 3 Doyen, Laurent 3 Fedyukovich, Grigory 3 Finkbeiner, Bernd 3 Fisman, Dana 3 Francalanza, Adrian 3 Gastin, Paul 3 Gnesi, Stefania 3 Hermanns, Holger 3 Hunt, Warren A. jun. 3 Iosif, Radu 3 Katz, Shmuel 3 Klaedtke, Felix 3 Kropf, Thomas 3 Kuncak, Viktor 3 Kurshan, Robert P. 3 La Torre, Salvatore 3 Legay, Axel 3 Malik, Sharad 3 Marchand, Hervé 3 Miné, Antoine 3 Nickovic, Dejan 3 Pace, Gordon J. 3 Pinisetty, Srinivas ...and 1,077 more Authors all top 5 Fields 540 Computer science (68-XX) 79 Mathematical logic and foundations (03-XX) 34 General and overarching topics; collections (00-XX) 22 Information and communication theory, circuits (94-XX) 15 Operations research, mathematical programming (90-XX) 15 Systems theory; control (93-XX) 11 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 5 Probability theory and stochastic processes (60-XX) 4 Numerical analysis (65-XX) 2 History and biography (01-XX) 2 Combinatorics (05-XX) 2 Commutative algebra (13-XX) 2 Operator theory (47-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 General algebraic systems (08-XX) 1 Number theory (11-XX) 1 Real functions (26-XX) 1 Ordinary differential equations (34-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Statistics (62-XX) 1 Mathematics education (97-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 376 Publications have been cited 2,576 times in 1,808 Documents Cited by ▼ Year ▼ Bounded model checking using satisfiability solving. Zbl 0985.68038 Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan 69 2001 Model checking of safety properties. Zbl 0995.68061 Kupferman, Orna; Vardi, Moshe Y. 56 2001 Property preserving abstractions for the verification of concurrent systems. Zbl 0829.68053 Loiseaux, C.; Graf, S.; Sifakis, J.; Bouajjani, A.; Bensalem, S. 47 1995 Faster algorithms for mean-payoff games. Zbl 1213.68430 Brim, L.; Chaloupka, J.; Doyen, L.; Gentilini, R.; Raskin, J. F. 46 2011 An improvement of McMillan’s unfolding algorithm. Zbl 1017.68085 Esparza, Javier; Römer, Stefan; Vogler, Walter 44 2002 Unified QBF certification and its applications. Zbl 1284.68516 Balabanov, Valeriy; Jiang, Jie-Hong R. 42 2012 A linear-time model-checking algorithm for the alternation-free modal mu- calculus. Zbl 0772.68038 Cleaveland, Rance; Steffen, Bernhard 40 1993 LSCs: Breathing life into message sequence charts. Zbl 0985.68033 Damm, Werner; Harel, David 39 2001 Using partial orders for the efficient verification of deadlock freedom and safety properties. Zbl 0772.68064 Godefroid, Patrice; Wolper, Pierre 38 1993 A stubborn attack on state explosion. Zbl 0783.68083 Valmari, Antti 36 1992 SMT-based model checking for recursive programs. Zbl 1358.68072 Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar 34 2016 From liveness to promptness. Zbl 1192.68416 Kupferman, Orna; Piterman, Nir; Vardi, Moshe Y. 34 2009 Using forward reachability analysis for verification of lossy channel systems. Zbl 1073.68675 Abdulla, Parosh Aziz; Collomb-Annichini, Aurore; Bouajjani, Ahmed; Jonsson, Bengt 32 2004 Performance analysis of probabilistic timed automata using digital clocks. Zbl 1105.68063 Kwiatkowska, Marta; Norman, Gethin; Parker, David; Sproston, Jeremy 32 2006 On the optimal reachability problem of weighted timed automata. Zbl 1129.68039 Bouyer, Patricia; Brihaye, Thomas; Bruyère, Véronique; Raskin, Jean-François 28 2007 An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps. Zbl 1110.68161 Bloem, Roderick; Gabow, Harold N.; Somenzi, Fabio 28 2006 Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245 Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano 27 2016 A game-based abstraction-refinement framework for Markov decision processes. Zbl 1233.90276 Kattenbelt, Mark; Kwiatkowska, Marta; Norman, Gethin; Parker, David 27 2010 Synthesis of opaque systems with static and dynamic masks. Zbl 1247.68161 Cassez, Franck; Dubreil, Jérémy; Marchand, Hervé 25 2012 Forward analysis of updatable timed automata. Zbl 1073.68041 Bouyer, Patricia 25 2004 Combining partial-order reductions with on-the-fly model-checking. Zbl 1425.68267 Peled, Doron 25 1996 A technique of state space search based on unfolding. Zbl 0829.68085 McMillan, K. L. 24 1995 Analysis of timed systems using time-abstracting bisimulations. Zbl 0971.68096 Tripakis, Stavros; Yovine, Sergio 24 2001 Minimum and maximum delay problems in real-time systems. Zbl 0777.68045 Courcoubetis, Costas; Yannakakis, Mihalis 24 1992 Data structures for symbolic multi-valued model-checking. Zbl 1109.68063 Chechik, Marsha; Gurfinkel, Arie; Devereux, Benet; Lai, Albert; Easterbrook, Steve 22 2006 Optimal infinite scheduling for multi-priced timed automata. Zbl 1133.68360 Bouyer, Patricia; Brinksma, Ed; Larsen, Kim G. 21 2008 HySAT: An efficient proof engine for bounded model checking of hybrid systems. Zbl 1116.68048 Fränzle, Martin; Herde, Christian 20 2007 Constructing invariants for hybrid systems. Zbl 1133.68365 Sankaranarayanan, Sriram; Sipma, Henny B.; Manna, Zohar 20 2008 Robust safety of timed automata. Zbl 1165.68392 De Wulf, Martin; Doyen, Laurent; Markey, Nicolas; Raskin, Jean-François 20 2008 Efficient detection of vacuity in temporal model checking. Zbl 0988.68111 Beer, Ilan; Ben-David, Shoham; Eisner, Cindy; Rodeh, Yoav 20 2001 Decision problems for lower/upper bound parametric timed automata. Zbl 1186.68245 Bozzelli, Laura; La Torre, Salvatore 20 2009 Checking timed Büchi automata emptiness efficiently. Zbl 1085.68083 Tripakis, Stavros; Yovine, Sergio; Bouajjani, Ahmed 20 2005 Monitoring hyperproperties. Zbl 1425.68254 Finkbeiner, Bernd; Hahn, Christopher; Stenger, Marvin; Tentrup, Leander 19 2019 Antichains and compositional algorithms for LTL synthesis. Zbl 1258.03046 Filiot, Emmanuel; Jin, Naiyong; Raskin, Jean-François 18 2011 A compositional modelling and analysis framework for stochastic hybrid systems. Zbl 1291.68293 Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter 18 2013 Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning. Zbl 1147.68053 Păsăreanu, Corina S.; Giannakopoulou, Dimitra; Bobaru, Mihaela Gheorghiu; Cobleigh, Jamieson M.; Barringer, Howard 18 2008 Deciding floating-point logic with abstract conflict driven clause learning. Zbl 1317.68110 Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel 18 2014 Efficiently solving quantified bit-vector formulas. Zbl 1284.03212 Wintersteiger, Christoph M.; Hamadi, Youssef; De Moura, Leonardo 18 2013 Abstractions for hybrid systems. Zbl 1133.68368 Tiwari, Ashish 17 2008 Automatic verification of competitive stochastic systems. Zbl 1291.68252 Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis 17 2013 Model checking for probabilistic timed automata. Zbl 1291.68265 Norman, Gethin; Parker, David; Sproston, Jeremy 17 2013 Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness. Zbl 1185.68405 Bagnara, Roberto; Hill, Patricia M.; Zaffanella, Enea 16 2009 Synthesising correct concurrent runtime monitors. Zbl 1323.68373 Francalanza, Adrian; Seychell, Aldrin 16 2015 Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022 Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen 16 2004 Monitorability for the Hennessy-Milner logic with recursion. Zbl 1370.68203 Francalanza, Adrian; Aceto, Luca; Ingolfsdottir, Anna 16 2017 Runtime enforcement of timed properties revisited. Zbl 1314.68102 Pinisetty, Srinivas; Falcone, Yliès; Jéron, Thierry; Marchand, Hervé; Rollet, Antoine; Nguena Timo, Omer 15 2014 Partial-order reduction in symbolic state-space exploration. Zbl 1001.68080 Alur, R.; Brayton, R. K.; Henzinger, T. A.; Qadeer, S.; Rajamani, S. K. 14 2001 Constraint-based verification of parameterized cache coherence protocols. Zbl 1073.68518 Delzanno, Giorgio 14 2003 Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Zbl 1341.68118 Demangeon, Romain; Honda, Kohei; Hu, Raymond; Neykova, Rumyana; Yoshida, Nobuko 14 2015 Robust online monitoring of signal temporal logic. Zbl 1370.68199 Deshmukh, Jyotirmoy V.; Donzé, Alexandre; Ghosh, Shromona; Jin, Xiaoqing; Juniwal, Garvit; Seshia, Sanjit A. 14 2017 Runtime enforcement monitors: Composition, synthesis, and enforcement abilities. Zbl 1219.68089 Falcone, Yliès; Mounier, Laurent; Fernandez, Jean-Claude; Richier, Jean-Luc 13 2011 Why does Astrée scale up? Zbl 1185.68241 Cousot, Patrick; Cousot, Radhia; Feret, Jérôme; Mauborgne, Laurent; Miné, Antoine; Rival, Xavier 13 2009 Conformance testing for real-time systems. Zbl 1180.68072 Krichen, Moez; Tripakis, Stavros 13 2009 Reducing concurrent analysis under a context bound to sequential analysis. Zbl 1186.68298 Lal, Akash; Reps, Thomas 13 2009 From LTL to deterministic automata. A safraless compositional approach. Zbl 1368.68233 Esparza, Javier; Křetínský, Jan; Sickert, Salomon 13 2016 Explaining counterexamples using causality. Zbl 1247.68158 Beer, Ilan; Ben-David, Shoham; Chockler, Hana; Orni, Avigail; Trefler, Richard 12 2012 Forest automata for verification of heap manipulation. Zbl 1284.68398 Habermehl, Peter; Holík, Lukáš; Rogalewicz, Adam; Šimáček, Jiří; Vojnar, Tomáš 12 2012 Pushdown module checking. Zbl 1209.68312 Bozzelli, Laura; Murano, Aniello; Peron, Adriano 11 2010 ModelPlex: verified runtime validation of verified cyber-physical system models. Zbl 1380.68282 Mitsch, Stefan; Platzer, André 11 2016 Shield synthesis. Zbl 1386.68101 Könighofer, Bettina; Alshiekh, Mohammed; Bloem, Roderick; Humphrey, Laura; Könighofer, Robert; Topcu, Ufuk; Wang, Chao 11 2017 Automating the addition of fault tolerance with discrete controller synthesis. Zbl 1186.68051 Girault, Alain; Rutten, Éric 11 2009 Dynamic partitioning in linear relation analysis: application to the verification of reactive systems. Zbl 1067.68091 Jeannet, B. 11 2003 Java-MaC: A run-time assurance approach for Java programs. Zbl 1073.68552 Kim, MoonZoo; Viswanathan, Mahesh; Kannan, Sampath; Lee, Insup; Sokolsky, Oleg 11 2004 An overview of the runtime verification tool Java PathExplorer. Zbl 1073.68549 Havelund, Klaus; Roşu, Grigore 11 2004 Bisimulation minimization and symbolic model checking. Zbl 1018.68052 Fisler, Kathi; Vardi, Moshe Y. 11 2002 Causal semantics for the algebra of connectors. Zbl 1207.68203 Bliudze, Simon; Sifakis, Joseph 11 2010 Quantitative monitoring of STL with edit distance. Zbl 1394.68230 Jakšić, Stefan; Bartocci, Ezio; Grosu, Radu; Nguyen, Thang; Ničković, Dejan 11 2018 SMT-based scenario verification for hybrid systems. Zbl 1284.03216 Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano 11 2013 Scalable offline monitoring of temporal specifications. Zbl 1380.68268 Basin, David; Caronni, Germano; Ereth, Sarah; Harvan, Matúš; Klaedtke, Felix; Mantel, Heiko 10 2016 Distributed synthesis for well-connected architectures. Zbl 1180.68056 Gastin, Paul; Sznajder, Nathalie; Zeitoun, Marc 10 2009 Computing differential invariants of hybrid systems as fixed points. Zbl 1180.93024 Platzer, André; Clarke, Edmund M. 10 2009 Checking finite traces using alternating automata. Zbl 1073.68053 Finkbeiner, Bernd; Sipma, Henny 10 2004 Some ways to reduce the space dimension in polyhedra computations. Zbl 1105.68107 Halbwachs, N.; Merchat, D.; Gonnord, L. 10 2006 Analyzing probabilistic pushdown automata. Zbl 1291.68226 Brázdil, Tomáš; Esparza, Javier; Kiefer, Stefan; Kučera, Antonín 10 2013 Computable fixpoints in well-structured symbolic model checking. Zbl 1291.68247 Bertrand, N.; Schnoebelen, P. 10 2013 Symbolic bounded synthesis. Zbl 1247.68163 Ehlers, Rüdiger 9 2012 From invariant checking to invariant inference using randomized search. Zbl 1358.68197 Sharma, Rahul; Aiken, Alex 9 2016 Specification and analysis of the AER/NCA active network protocol suite in real-time Maude. Zbl 1109.68010 Ölveczky, Peter Csaba; Meseguer, José; Talcott, Carolyn L. 9 2006 Hybrid systems: From verification to falsification by combining motion planning and discrete search. Zbl 1192.68692 Plaku, Erion; Kavraki, Lydia E.; Vardi, Moshe Y. 9 2009 Two case studies of semantics execution in Maude: CCS and LOTOS. Zbl 1086.68552 Verdejo, Alberto; Martí-Oliet, Narciso 9 2005 Automata-based symbolic string analysis for vulnerability detection. Zbl 1291.68272 Yu, Fang; Alkhalaf, Muath; Bultan, Tevfik; Ibarra, Oscar H. 9 2014 A zonotopic framework for functional abstractions. Zbl 1331.68050 Goubault, Eric; Putot, Sylvie 9 2015 Resolution proof transformation for compression and interpolation. Zbl 1317.68123 Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei 9 2014 An efficient SMT solver for string constraints. Zbl 1404.68135 Liang, Tianyi; Reynolds, Andrew; Tsiskaridze, Nestan; Tinelli, Cesare; Barrett, Clark; Deters, Morgan 8 2016 MSO logics for weighted timed automata. Zbl 1258.68089 Quaas, Karin 8 2011 Timed verification of the generic architecture of a memory circuit using parametric timed automata. Zbl 1165.68401 Chevallier, Remy; Encrenaz-Tiphene, Emmanuelle; Fribourg, Laurent; Xu, Weiwen 8 2009 Local proofs for global safety properties. Zbl 1176.68118 Cohen, Ariel; Namjoshi, Kedar S. 8 2009 Bayesian statistical model checking with application to Stateflow/Simulink verification. Zbl 1291.68273 Zuliani, Paolo; Platzer, André; Clarke, Edmund M. 8 2013 A survey of challenges for runtime verification from advanced application domains (beyond software). Zbl 1425.68268 Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; Bartocci, Ezio; Bianculli, Domenico; Colombo, Christian; Falcone, Yliès; Francalanza, Adrian; Krstić, Srđan; Lourenço, João M.; Nickovic, Dejan; Pace, Gordon J.; Rufino, Jose; Signoles, Julien; Traytel, Dmitriy; Weiss, Alexander 8 2019 SMT proof checking using a logical framework. Zbl 1284.68521 Stump, Aaron; Oe, Duckki; Reynolds, Andrew; Hadarean, Liana; Tinelli, Cesare 8 2013 Organising LTL monitors over distributed systems with a global clock. Zbl 1380.68272 Colombo, Christian; Falcone, Yliès 7 2016 Safely composing security protocols. Zbl 1165.68358 Cortier, Véronique; Delaune, Stéphanie 7 2009 Parallelizing the \(\text{Mur}\varphi\) verifier. Zbl 1001.68073 Stern, Ulrich; Dill, David 7 2001 A new heuristic for bad cycle detection using BDDs. Zbl 1001.68074 Hardin, R. H.; Kurshan, R. P.; Shukla, S. K.; Vardi, M. Y. 7 2001 Relaxed visibility enhances partial order reduction. Zbl 0995.68060 Peled, Doron; Valmari, Antti; Kokkarinen, Ilkka 7 2001 From pre-historic to post-modern symbolic model checking. Zbl 1074.68036 Henzinger, Thomas A.; Kupferman, Orna; Qadeer, Shaz 7 2003 Static analysis for state-space reductions preserving temporal logics. Zbl 1073.68055 Yorav, Karen; Grumberg, Orna 7 2004 Compositional checking of satisfaction. Zbl 0776.68083 Andersen, Henrik Reif; Winskel, Glynn 7 1992 An extension of the inverse method to probabilistic timed automata. Zbl 1291.68240 André, Étienne; Fribourg, Laurent; Sproston, Jeremy 7 2013 Code aware resource management. Zbl 1291.68137 Chatterjee, Krishnendu; De Alfaro, Luca; Faella, Marco; Majumdar, Rupak; Raman, Vishwanath 7 2013 Reluplex: a calculus for reasoning about deep neural networks. Zbl 1522.68328 Katz, Guy; Barrett, Clark; Dill, David L.; Julian, Kyle; Kochenderfer, Mykel J. 2 2022 LTL model checking of self modifying code. Zbl 07683087 Touili, Tayssir; Ye, Xin 1 2022 Functional synthesis via input-output separation. Zbl 07683088 Chakraborty, Supratik; Fried, Dror; Tabajara, Lucas M.; Vardi, Moshe Y. 1 2022 Certifying proofs for SAT-based model checking. Zbl 1522.68319 Griggio, Alberto; Roveri, Marco; Tonetta, Stefano 5 2021 On solving quantified bit-vector constraints using invertibility conditions. Zbl 1519.68236 Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare 3 2021 A relational shape abstract domain. Zbl 1522.68156 Illous, Hugo; Lemerre, Matthieu; Rival, Xavier 2 2021 Automatic verification of concurrent stochastic systems. Zbl 1505.68025 Kwiatkowska, Marta; Norman, Gethin; Parker, David; Santos, Gabriel 2 2021 Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations. Zbl 1522.68715 Bloem, Roderick; Braud-Santoni, Nicolas; Hadzic, Vedad; Egly, Uwe; Lonsing, Florian; Seidl, Martina 1 2021 Temporal prophecy for proving temporal properties of infinite-state systems. Zbl 1522.68340 Padon, Oded; Hoenicke, Jochen; McMillan, Kenneth L.; Podelski, Andreas; Sagiv, Mooly; Shoham, Sharon 1 2021 Faster algorithms for quantitative verification in bounded treewidth graphs. Zbl 1522.68301 Chatterjee, Krishnendu; Ibsen-Jensen, Rasmus; Pavlogiannis, Andreas 1 2021 Gray-box monitoring of hyperproperties with an application to privacy. Zbl 1502.68187 Stucki, Sandro; Sánchez, César; Schneider, Gerardo; Bonakdarpour, Borzoo 1 2021 Abstraction and subsumption in modular verification of C programs. Zbl 1505.68023 Beringer, Lennart; Appel, Andrew W. 1 2021 Boolean functional synthesis: hardness and practical algorithms. Zbl 1519.68128 Akshay, S.; Chakraborty, Supratik; Goel, Shubham; Kulal, Sumith; Shah, Shetal 1 2021 First-order temporal logic monitoring with BDDs. Zbl 1506.68055 Havelund, Klaus; Peled, Doron; Ulus, Dogan 6 2020 Learning inductive invariants by sampling from frequency distributions. Zbl 1506.68054 Fedyukovich, Grigory; Kaufman, Samuel J.; Bodík, Rastislav 6 2020 Parameterized verification of algorithms for oblivious robots on a ring. Zbl 1506.68058 Sangnier, Arnaud; Sznajder, Nathalie; Potop-Butucaru, Maria; Tixeuil, Sébastien 2 2020 Incremental column-wise verification of arithmetic circuits using computer algebra. Zbl 1506.68056 Kaufmann, Daniela; Biere, Armin; Kauers, Manuel 1 2020 Exact quantitative probabilistic model checking through rational search. Zbl 1506.68057 Mathur, Umang; Bauer, Matthew S.; Chadha, Rohit; Sistla, A. Prasad; Viswanathan, Mahesh 1 2020 Monitoring hyperproperties. Zbl 1425.68254 Finkbeiner, Bernd; Hahn, Christopher; Stenger, Marvin; Tentrup, Leander 19 2019 A survey of challenges for runtime verification from advanced application domains (beyond software). Zbl 1425.68268 Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; Bartocci, Ezio; Bianculli, Domenico; Colombo, Christian; Falcone, Yliès; Francalanza, Adrian; Krstić, Srđan; Lourenço, João M.; Nickovic, Dejan; Pace, Gordon J.; Rufino, Jose; Signoles, Julien; Traytel, Dmitriy; Weiss, Alexander 8 2019 TeLEx: learning signal temporal logic from positive examples using tightness metric. Zbl 1425.68349 Jha, Susmit; Tiwari, Ashish; Seshia, Sanjit A.; Sahai, Tuhin; Shankar, Natarajan 5 2019 Alloy*: a general-purpose higher-order relational constraint solver. Zbl 1425.68264 Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel 5 2019 Refutation-based synthesis in SMT. Zbl 1427.68051 Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan 5 2019 Some complexity results for stateful network verification. Zbl 1425.68248 Alpernas, Kalev; Panda, Aurojit; Rabinovich, Alexander; Sagiv, Mooly; Shenker, Scott; Shoham, Sharon; Velner, Yaron 4 2019 Probabilistic black-box reachability checking (extended version). Zbl 1425.68247 Aichernig, Bernhard K.; Tappler, Martin 4 2019 Almost event-rate independent monitoring. Zbl 1425.68249 Basin, David; Bhatt, Bhargav Nagaraja; Krstić, Srđan; Traytel, Dmitriy 4 2019 Synthesizing adaptive test strategies from temporal logic specifications. Zbl 1427.68160 Bloem, Roderick; Fey, Goerschwin; Greif, Fabian; Könighofer, Robert; Pill, Ingo; Riener, Heinz; Röck, Franz 2 2019 Template polyhedra and bilinear optimization. Zbl 1426.65079 Gronski, Jessica; Ben Sassi, Mohamed-Amin; Becker, Stephen; Sankaranarayanan, Sriram 2 2019 Statistical verification of PCTL using antithetic and stratified samples. Zbl 1425.68270 Wang, Yu; Roohi, Nima; West, Matthew; Viswanathan, Mahesh; Dullerud, Geir E. 1 2019 Annotation guided collection of context-sensitive parallel execution profiles. Zbl 1425.68056 Benavides, Zachary; Vora, Keval; Gupta, Rajiv; Zhang, Xiangyu 1 2019 Quantitative static analysis of communication protocols using abstract Markov chains. Zbl 1425.68078 Ouadjaout, Abdelraouf; Miné, Antoine 1 2019 A new abstraction framework for affine transformers. Zbl 1425.68084 Sharma, Tushar; Reps, Thomas 1 2019 Quantitative monitoring of STL with edit distance. Zbl 1394.68230 Jakšić, Stefan; Bartocci, Ezio; Grosu, Radu; Nguyen, Thang; Ničković, Dejan 11 2018 Solving parity games via priority promotion. Zbl 1390.68332 Benerecetti, Massimo; Dell’Erba, Daniele; Mogavero, Fabio 5 2018 Finite-trace linear temporal logic: coinductive completeness. Zbl 1394.68237 Roşu, Grigore 3 2018 Automated verification of automata communicating via FIFO and bag buffers. Zbl 1392.68224 Akroun, Lakhdar; Salaün, Gwen 3 2018 Algorithmic games for full ground references. Zbl 1392.68147 Murawski, Andrzej S.; Tzevelekos, Nikos 3 2018 Validating numerical semidefinite programming solvers for polynomial invariants. Zbl 1425.68081 Roux, Pierre; Voronin, Yuen-Lam; Sankaranarayanan, Sriram 3 2018 Theory and methodology of assumption/commitment based system interface specification and architectural contracts. Zbl 1392.68238 Broy, Manfred 2 2018 Wireless protocol validation under uncertainty. Zbl 1394.68027 Shi, Jinghao; Lahiri, Shuvendu K.; Chandra, Ranveer; Challen, Geoffrey 2 2018 On relative and probabilistic finite counterability. Zbl 1390.68433 Kupferman, Orna; Vardi, Gal 1 2018 Conditions of contracts for separating responsibilities in heterogeneous systems. Zbl 1390.68442 Westman, Jonas; Nyberg, Mattias 1 2018 On the complexity of monitoring Orchids signatures, and recurrence equations. Zbl 1394.68180 Goubault-Larrecq, Jean; Lachance, Jean-Philippe 1 2018 Enforcing termination of interprocedural analysis. Zbl 1425.68083 Schulze Frielinghaus, Stefan; Seidl, Helmut; Vogler, Ralf 1 2018 An improved algorithm for the control synthesis of nonlinear sampled switched systems. Zbl 1428.93053 Le Coënt, Adrien; Alexandre dit Sandretto, Julien; Chapoutot, Alexandre; Fribourg, Laurent 1 2018 Improving the results of program analysis by abstract interpretation beyond the decreasing sequence. Zbl 1425.68064 Boutonnet, Rémy; Halbwachs, Nicolas 1 2018 Monitorability for the Hennessy-Milner logic with recursion. Zbl 1370.68203 Francalanza, Adrian; Aceto, Luca; Ingolfsdottir, Anna 16 2017 Robust online monitoring of signal temporal logic. Zbl 1370.68199 Deshmukh, Jyotirmoy V.; Donzé, Alexandre; Ghosh, Shromona; Jin, Xiaoqing; Juniwal, Garvit; Seshia, Sanjit A. 14 2017 Shield synthesis. Zbl 1386.68101 Könighofer, Bettina; Alshiekh, Mohammed; Bloem, Roderick; Humphrey, Laura; Könighofer, Robert; Topcu, Ufuk; Wang, Chao 11 2017 Solving quantified linear arithmetic by counterexample-guided instantiation. Zbl 1377.68138 Reynolds, Andrew; King, Tim; Kuncak, Viktor 7 2017 Cardinality constraints for arrays (decidability results and applications). Zbl 1377.68125 Alberti, F.; Ghilardi, S.; Pagani, E. 7 2017 Model checking parameterized asynchronous shared-memory systems. Zbl 1360.68584 Durand-Gasselin, Antoine; Esparza, Javier; Ganty, Pierre; Majumdar, Rupak 7 2017 Quantifying conformance using the Skorokhod metric. Zbl 1360.68629 Deshmukh, Jyotirmoy V.; Majumdar, Rupak; Prabhu, Vinayak S. 7 2017 Percentile queries in multi-dimensional Markov decision processes. Zbl 1360.68518 Randour, Mickael; Raskin, Jean-François; Sankur, Ocan 7 2017 Propagation based local search for bit-precise reasoning. Zbl 1377.68134 Niemetz, Aina; Preiner, Mathias; Biere, Armin 6 2017 \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Zbl 1380.68279 Konnov, Igor; Lazić, Marijana; Veith, Helmut; Widder, Josef 5 2017 Predictive runtime enforcement. Zbl 1370.68207 Pinisetty, Srinivas; Preoteasa, Viorel; Tripakis, Stavros; Jéron, Thierry; Falcone, Yliès; Marchand, Hervé 5 2017 Reachability computation for polynomial dynamical systems. Zbl 1360.93084 Dreossi, Tommaso; Dang, Thao; Piazza, Carla 5 2017 raSAT: an SMT solver for polynomial constraints. Zbl 1377.68140 Tung, Vu Xuan; Khanh, To Van; Ogawa, Mizuhito 4 2017 Compositional entailment checking for a fragment of separation logic. Zbl 1377.68073 Enea, Constantin; Lengál, Ondřej; Sighireanu, Mihaela; Vojnar, Tomáš 4 2017 Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Zbl 1370.68195 Ahrendt, Wolfgang; Chimento, Jesús Mauricio; Pace, Gordon J.; Schneider, Gerardo 4 2017 Z3str2: an efficient solver for strings, regular expressions, and length constraints. Zbl 1360.68773 Zheng, Yunhui; Ganesh, Vijay; Subramanian, Sanu; Tripp, Omer; Berzish, Murphy; Dolby, Julian; Zhang, Xiangyu 4 2017 Empirical software metrics for benchmarking of verification tools. Zbl 1360.68371 Demyanova, Yulia; Pani, Thomas; Veith, Helmut; Zuleger, Florian 3 2017 Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles. Zbl 1370.68287 Phan, Dung; Yang, Junxing; Grosu, Radu; Smolka, Scott A.; Stoller, Scott D. 2 2017 Formal analysis and offline monitoring of electronic exams. Zbl 1370.68205 Kassem, Ali; Falcone, Yliès; Lafourcade, Pascal 2 2017 Symbolic trajectory evaluation for word-level verification: theory and implementation. Zbl 1360.68582 Chakraborty, Supratik; Khasidashvili, Zurab; Seger, Carl-Johan H.; Gajavelly, Rajkumar; Haldankar, Tanmay; Chhatani, Dinesh; Mistry, Rakesh 2 2017 Preface of the special issue in memoriam Helmut Veith. Zbl 1384.00074 1 2017 On compiling Boolean circuits optimized for secure multi-party computation. Zbl 1386.68020 Büscher, Niklas; Franz, Martin; Holzer, Andreas; Veith, Helmut; Katzenbeisser, Stefan 1 2017 New techniques for linear arithmetic: cubes and equalities. Zbl 1377.68128 Bromberger, Martin; Weidenbach, Christoph 1 2017 NP-completeness of small conflict set generation for congruence closure. Zbl 1377.68090 Fellner, Andreas; Fontaine, Pascal; Paleo, Bruno Woltzenlogel 1 2017 From non-preemptive to preemptive scheduling using synchronization synthesis. Zbl 1360.68346 Černý, Pavol; Clarke, Edmund M.; Henzinger, Thomas A.; Radhakrishna, Arjun; Ryzhyk, Leonid; Samanta, Roopsha; Tarrach, Thorsten 1 2017 SMT-based model checking for recursive programs. Zbl 1358.68072 Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar 34 2016 Infinite-state invariant checking with IC3 and predicate abstraction. Zbl 1368.68245 Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano 27 2016 From LTL to deterministic automata. A safraless compositional approach. Zbl 1368.68233 Esparza, Javier; Křetínský, Jan; Sickert, Salomon 13 2016 ModelPlex: verified runtime validation of verified cyber-physical system models. Zbl 1380.68282 Mitsch, Stefan; Platzer, André 11 2016 Scalable offline monitoring of temporal specifications. Zbl 1380.68268 Basin, David; Caronni, Germano; Ereth, Sarah; Harvan, Matúš; Klaedtke, Felix; Mantel, Heiko 10 2016 From invariant checking to invariant inference using randomized search. Zbl 1358.68197 Sharma, Rahul; Aiken, Alex 9 2016 An efficient SMT solver for string constraints. Zbl 1404.68135 Liang, Tianyi; Reynolds, Andrew; Tsiskaridze, Nestan; Tinelli, Cesare; Barrett, Clark; Deters, Morgan 8 2016 Organising LTL monitors over distributed systems with a global clock. Zbl 1380.68272 Colombo, Christian; Falcone, Yliès 7 2016 Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components. Zbl 1404.68204 Wijs, Anton; Katoen, Joost-Pieter; Bošnački, Dragan 5 2016 Decentralised LTL monitoring. Zbl 1392.68229 Bauer, Andreas; Falcone, Yliès 5 2016 The spirit of ghost code. Zbl 1358.68070 Filliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei 4 2016 A layered algorithm for quantifier elimination from linear modular constraints. Zbl 1368.68332 John, Ajith K.; Chakraborty, Supratik 3 2016 A search-based procedure for nonlinear real arithmetic. Zbl 1358.68149 Tiwari, Ashish; Lincoln, Patrick 2 2016 Synthesis of large dynamic concurrent programs from dynamic specifications. Zbl 1392.68143 Attie, Paul C. 2 2016 Abstraction and mining of traces to explain concurrency bugs. Zbl 1380.68107 Tabaei Befrouei, Mitra; Wang, Chao; Weissenbacher, Georg 1 2016 Synthesising correct concurrent runtime monitors. Zbl 1323.68373 Francalanza, Adrian; Seychell, Aldrin 16 2015 Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Zbl 1341.68118 Demangeon, Romain; Honda, Kohei; Hu, Raymond; Neykova, Rumyana; Yoshida, Nobuko 14 2015 A zonotopic framework for functional abstractions. Zbl 1331.68050 Goubault, Eric; Putot, Sylvie 9 2015 On recursion-free Horn clauses and Craig interpolation. Zbl 1322.68134 Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor 7 2015 Under-approximating loops in C programs for fast counterexample detection. Zbl 1322.68054 Kroening, Daniel; Lewis, Matt; Weissenbacher, Georg 7 2015 Generating models of infinite-state communication protocols using regular inference with abstraction. Zbl 1322.68131 Aarts, Fides; Jonsson, Bengt; Uijen, Johan; Vaandrager, Frits 6 2015 Program repair without regret. Zbl 1322.68056 von Essen, Christian; Jobstmann, Barbara 5 2015 Monitoring of temporal first-order properties with aggregations. Zbl 1323.68362 Basin, David; Klaedtke, Felix; Marinovic, Srdjan; Zălinescu, Eugen 5 2015 A game approach to determinize timed automata. Zbl 1323.68337 Bertrand, Nathalie; Stainer, Amélie; Jéron, Thierry; Krichen, Moez 5 2015 Extended symbolic finite automata and transducers. Zbl 1341.68085 D’Antoni, Loris; Veanes, Margus 4 2015 Runtime verification with minimal intrusion through parallelism. Zbl 1323.68363 Berkovich, Shay; Bonakdarpour, Borzoo; Fischmeister, Sebastian 4 2015 Proving mutual termination. Zbl 1322.68052 Elenbogen, Dima; Katz, Shmuel; Strichman, Ofer 3 2015 Optimization techniques for Craig interpolant compaction in unbounded model checking. Zbl 1341.68117 Cabodi, Gianpiero; Loiacono, Carmelo; Vendraminetto, Danilo 3 2015 Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists. Zbl 1322.68121 Garg, Pranav; Löding, Christof; Madhusudan, P.; Neider, Daniel 2 2015 ...and 276 more Documents all cited Publications top 5 cited Publications all top 5 Cited by 2,798 Authors 23 Chatterjee, Krishnendu 23 Kröning, Daniel 22 Larsen, Kim Guldstrand 21 Kupferman, Orna 21 Kwiatkowska, Marta Z. 20 Cimatti, Alessandro 20 Vardi, Moshe Ya’akov 19 Bouyer, Patricia 19 Zimmermann, Martín G. 17 André, Étienne 17 Baier, Christel 17 Francalanza, Adrian 17 Markey, Nicolas 17 Norman, Gethin 17 Raskin, Jean-François 16 Katoen, Joost-Pieter 16 Legay, Axel 16 Meseguer Guaita, José 15 Abdulla, Parosh Aziz 15 Barrett, Clark W. 14 Aceto, Luca 14 Basin, David A. 14 Beyersdorff, Olaf 14 Falcone, Yliès 14 Griggio, Alberto 14 Grumberg, Orna 14 Peled, Doron A. 13 Křetínský, Jan 13 Murano, Aniello 13 Tonetta, Stefano 12 Finkel, Alain 12 Randour, Mickael 11 Bérard, Béatrice 11 Biere, Armin 11 Bloem, Roderick 11 Lime, Didier 11 Reynolds, Andrew 11 Tinelli, Cesare 11 van de Pol, Jan Cornelis 10 Bonakdarpour, Borzoo 10 Bozzelli, Laura 10 Droste, Manfred 10 Fahrenberg, Uli 10 Ingólfsdóttir, Anna 10 Platzer, André 10 Shoham, Sharon 10 Srba, Jiří 10 Willemse, Tim A. C. 9 Baldan, Paolo 9 Beneš, Nikola 9 Fränzle, Martin 9 Haddad, Serge 9 Henzinger, Thomas A. 9 Jéron, Thierry 9 King, Andy 9 Kobayashi, Naoki 9 Lange, Martin 9 Roux, Olivier H. 9 Rümmer, Philipp 9 Sharygina, Natasha 9 Zamani, Majid 8 Bartocci, Ezio 8 Bertrand, Nathalie 8 Brim, Luboš 8 Chakraborty, Supratik 8 Doyen, Laurent 8 Finkbeiner, Bernd 8 Fribourg, Laurent 8 Gastin, Paul 8 Haar, Stefan 8 Holík, Lukáš 8 Klaedtke, Felix 8 Konnov, Igor V. 8 Sproston, Jeremy 8 Strichman, Ofer 8 Subramani, Krishnan 8 Trivedi, Ashutosh 8 Weinert, Alexander 8 Weissenbacher, Georg 8 Widder, Josef 8 Zhang, Lijun 7 Abate, Alessandro 7 Atig, Mohamed Faouzi 7 Brihaye, Thomas 7 Chew, Leroy 7 Chockler, Hana 7 Garavel, Hubert 7 Jensen, Peter Gjøl 7 Jobstmann, Barbara 7 Khomenko, Victor 7 Koutny, Maciej 7 Lafortune, Stéphane 7 Lavaei, Abolfazl 7 Lengál, Ondřej 7 Li, Yongming 7 Marchand, Hervé 7 Monmege, Benjamin 7 Montanari, Angelo 7 Neider, Daniel 7 Olveczky, Peter Csaba ...and 2,698 more Authors all top 5 Cited in 114 Journals 201 Formal Methods in System Design 132 Theoretical Computer Science 82 Information and Computation 55 Formal Aspects of Computing 53 Journal of Automated Reasoning 52 Logical Methods in Computer Science 45 Acta Informatica 36 Journal of Logical and Algebraic Methods in Programming 30 Automatica 21 Journal of Computer and System Sciences 19 Information Processing Letters 19 Discrete Event Dynamic Systems 16 Science of Computer Programming 16 The Journal of Logic and Algebraic Programming 15 Nonlinear Analysis. Hybrid Systems 14 International Journal of Foundations of Computer Science 13 Artificial Intelligence 10 ACM Transactions on Computational Logic 9 Programming and Computer Software 9 Annals of Mathematics and Artificial Intelligence 9 Fundamenta Informaticae 7 Real-Time Systems 7 Constraints 6 MSCS. Mathematical Structures in Computer Science 6 Distributed Computing 6 Mathematical Problems in Engineering 6 Theory of Computing Systems 6 RAIRO. Theoretical Informatics and Applications 6 Journal of Applied Logic 5 Fuzzy Sets and Systems 5 Algorithmica 5 International Journal of Approximate Reasoning 5 Theory and Practice of Logic Programming 5 Journal of Applied Mathematics 4 Information Sciences 4 Journal of Symbolic Computation 4 Journal of Computer Science and Technology 4 Higher-Order and Symbolic Computation 4 Computer Languages, Systems & Structures 4 Algorithms 3 Discrete Applied Mathematics 3 Systems & Control Letters 3 Journal of Logic, Language and Information 3 The Bulletin of Symbolic Logic 3 European Journal of Control 3 Journal of the ACM 3 Sibirskie Èlektronnye Matematicheskie Izvestiya 3 Journal of Satisfiability, Boolean Modeling and Computation 3 Modelirovanie i Analiz Informatsionnykh Sistem 2 International Journal of Control 2 International Journal of General Systems 2 Computing 2 Studia Logica 2 International Journal of Parallel Programming 2 Journal of Parallel and Distributed Computing 2 Journal of Computer and Systems Sciences International 2 Journal of Functional Programming 2 Soft Computing 2 Journal of Systems Science and Complexity 2 Mathematics in Computer Science 2 Science China. Information Sciences 2 Frontiers of Computer Science 2 Computer Science Review 1 ACM Computing Surveys 1 International Journal of Theoretical Physics 1 Linear and Multilinear Algebra 1 Rocky Mountain Journal of Mathematics 1 Journal of Optimization Theory and Applications 1 Mathematics and Computers in Simulation 1 Rendiconti dell’Istituto di Matematica dell’Università di Trieste 1 SIAM Journal on Computing 1 Software. Practice & Experience 1 Synthese 1 Circuits, Systems, and Signal Processing 1 Annals of Pure and Applied Logic 1 Asia-Pacific Journal of Operational Research 1 Journal of Cryptology 1 Random Structures & Algorithms 1 Neural Computation 1 Computational Geometry 1 International Journal of Algebra and Computation 1 Numerical Algorithms 1 Automation and Remote Control 1 Journal of Statistical Computation and Simulation 1 Linear Algebra and its Applications 1 SIAM Review 1 International Journal of Robust and Nonlinear Control 1 Advances in Engineering Software 1 Cybernetics and Systems Analysis 1 Journal of Applied Non-Classical Logics 1 The Journal of Artificial Intelligence Research (JAIR) 1 International Transactions in Operational Research 1 Science in China. Series E 1 Journal of Automata, Languages and Combinatorics 1 Journal of Combinatorial Optimization 1 Journal of Applied Mathematics and Decision Sciences 1 Mathematical and Computer Modelling of Dynamical Systems 1 Discrete Dynamics in Nature and Society 1 LMS Journal of Computation and Mathematics 1 Natural Computing ...and 14 more Journals all top 5 Cited in 38 Fields 1,680 Computer science (68-XX) 370 Mathematical logic and foundations (03-XX) 135 Systems theory; control (93-XX) 119 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 71 Operations research, mathematical programming (90-XX) 35 Information and communication theory, circuits (94-XX) 25 Biology and other natural sciences (92-XX) 21 Numerical analysis (65-XX) 19 Combinatorics (05-XX) 18 Probability theory and stochastic processes (60-XX) 8 General and overarching topics; collections (00-XX) 6 Order, lattices, ordered algebraic structures (06-XX) 6 Quantum theory (81-XX) 4 Real functions (26-XX) 4 Statistics (62-XX) 3 Number theory (11-XX) 3 Linear and multilinear algebra; matrix theory (15-XX) 3 Measure and integration (28-XX) 3 Ordinary differential equations (34-XX) 3 Dynamical systems and ergodic theory (37-XX) 3 Convex and discrete geometry (52-XX) 2 Calculus of variations and optimal control; optimization (49-XX) 1 History and biography (01-XX) 1 Field theory and polynomials (12-XX) 1 Category theory; homological algebra (18-XX) 1 Group theory and generalizations (20-XX) 1 Topological groups, Lie groups (22-XX) 1 Partial differential equations (35-XX) 1 Difference and functional equations (39-XX) 1 Harmonic analysis on Euclidean spaces (42-XX) 1 Integral transforms, operational calculus (44-XX) 1 Differential geometry (53-XX) 1 General topology (54-XX) 1 Algebraic topology (55-XX) 1 Manifolds and cell complexes (57-XX) 1 Mechanics of particles and systems (70-XX) 1 Fluid mechanics (76-XX) 1 Mathematics education (97-XX) Citations by Year