Formal Aspects of Computing Short Title: Formal Asp. Comput. Publisher: Association for Computing Machinery (ACM), New York, NY ISSN: 0934-5043; 1433-299X/e Online: https://dl.acm.org/loi/fachttp://link.springer.com/journal/volumesAndIssues/165 Comments: Journal; Indexed cover-to-cover Documents Indexed: 881 Publications (since 1989) References Indexed: 630 Publications with 21,981 References. all top 5 Latest Issues 34, No. 3-4 (2022) 34, No. 2 (2022) 34, No. 1 (2022) 33, No. 6 (2021) 33, No. 4-5 (2021) 33, No. 3 (2021) 33, No. 2 (2021) 33, No. 1 (2021) 32, No. 4-6 (2020) 32, No. 2-3 (2020) 32, No. 1 (2020) 31, No. 6 (2019) 31, No. 5 (2019) 31, No. 4 (2019) 31, No. 3 (2019) 31, No. 2 (2019) 31, No. 1 (2019) 30, No. 6 (2018) 30, No. 5 (2018) 30, No. 3-4 (2018) 30, No. 2 (2018) 30, No. 1 (2018) 29, No. 6 (2017) 29, No. 5 (2017) 29, No. 4 (2017) 29, No. 3 (2017) 29, No. 2 (2017) 29, No. 1 (2017) 28, No. 6 (2016) 28, No. 5 (2016) 28, No. 4 (2016) 28, No. 3 (2016) 28, No. 2 (2016) 28, No. 1 (2016) 27, No. 5-6 (2015) 27, No. 4 (2015) 27, No. 3 (2015) 27, No. 2 (2015) 27, No. 1 (2015) 26, No. 6 (2014) 26, No. 5 (2014) 26, No. 4 (2014) 26, No. 3 (2014) 26, No. 2 (2014) 26, No. 1 (2014) 25, No. 6 (2013) 25, No. 5 (2013) 25, No. 4 (2013) 25, No. 3 (2013) 25, No. 2 (2013) 25, No. 1 (2013) 24, No. 4-6 (2012) 24, No. 3 (2012) 24, No. 2 (2012) 24, No. 1 (2012) 23, No. 6 (2011) 23, No. 5 (2011) 23, No. 4 (2011) 23, No. 3 (2011) 23, No. 2 (2011) 23, No. 1 (2011) 22, No. 6 (2010) 22, No. 5 (2010) 22, No. 3-4 (2010) 22, No. 2 (2010) 22, No. 1 (2010) 21, No. 6 (2009) 21, No. 5 (2009) 21, No. 4 (2009) 21, No. 3 (2009) 21, No. 1-2 (2009) 20, No. 6 (2008) 20, No. 4-5 (2008) 20, No. 3 (2008) 20, No. 2 (2008) 19, No. 4 (2007) 19, No. 3 (2007) 19, No. 2 (2007) 19, No. 1 (2007) 18, No. 4 (2006) 18, No. 3 (2006) 18, No. 2 (2006) 18, No. 1 (2006) 17, No. 4 (2005) 17, No. 3 (2005) 17, No. 2 (2005) 17, No. 1 (2005) 16, No. 4 (2004) 16, No. 3 (2004) 16, No. 2 (2004) 16, No. 1 (2004) 15, No. 4 (2003) 15, No. 2-3 (2003) 15, No. 1 (2003) 14, No. 4 (2002) 14, No. 3 (2002) 14, No. 2 (2002) 14, No. 1 (2002) 13, No. 6 (2002) 13, No. 3-5 (2002) ...and 62 more Volumes all top 5 Authors 20 Woodcock, James C. P. 18 Cavalcanti, Ana 15 Hesselink, Wim H. 14 Derrick, John 12 Hayes, Ian J. 12 Smith, Graeme 11 Back, Ralph-Johan 10 Boiten, Eerke A. 10 Jones, Cliff B. 9 Wehrheim, Heike 8 Dong, JinSong 7 Bergstra, Jan A. 7 Bowen, Jonathan P. 7 He, Jifeng 7 Liu, Zhiming 7 Morgan, Carroll C. 7 Reeves, Steve 7 Roscoe, Andrew William 7 Sampaio, Augusto C. A. 7 Schneider, Steve A. 6 Banach, Richard 6 Colvin, Robert J. 6 Dongol, Brijesh 6 Hennessy, Matthew C. B. 6 Henson, Martin C. 6 Ipate, Florentin 5 Baeten, Jos C. M. 5 Börger, Egon 5 Fidge, Colin J. 5 Groote, Jan Friso 5 Kwiatkowska, Marta Z. 5 Maibaum, Thomas Stephen Edward 5 Oliveira, Marcel 5 Paige, Richard F. 5 Pang, Jun 5 Schellhorn, Gerhard 5 Treharne, Helen 5 Zhu, Huibiao 4 Bowman, Howard 4 Bozzano, Marco 4 Brooke, Phillip J. 4 Fiadeiro, José Luiz 4 Hoang, Thai Son 4 Holcombe, Mike 4 Katoen, Joost-Pieter 4 Kröning, Daniel 4 Larsen, Peter Gorm 4 Leino, K. Rustan M. 4 McIver, Annabelle K. 4 Meinicke, Larissa A. 4 Norman, Gethin 4 Olderog, Ernst-Rüdiger 4 Owe, Olaf 4 Pym, David J. 4 Tahar, Sofiène 4 Tofts, Chris 4 Winter, Kirsten 4 Zhan, Naijun 3 Aichernig, Bernhard K. 3 America, Pierre 3 Apt, Krzysztof Rafal 3 Bird, Richard S. 3 Blandford, Ann 3 Bornat, Richard 3 Brink, Chris 3 Broy, Manfred 3 Butterfield, Andrew 3 Calder, Muffy 3 Chechik, Marsha 3 Cimatti, Alessandro 3 Collinson, Matthew 3 Curzon, Paul 3 Davies, Jim 3 de Boer, Frank S. 3 de Lara, Juan 3 de Vink, Erik P. 3 Doherty, Simon 3 Fränzle, Martin 3 Frappier, Marc 3 Gabarró, Joaquim 3 Gardiner, Paul H. B. 3 Gnesi, Stefania 3 Gomez, Rodolfo 3 Hallerstede, Stefan 3 Hansen, Michael Reichhardt 3 Harman, Mark 3 Hasan, Osman 3 Haxthausen, Anne Elisabeth 3 Hennicker, Rolf 3 Hierons, Robert Mark 3 Inverardi, Paola 3 Jifeng, He 3 Jonsson, Bengt 3 Julliand, Jacques 3 King, Steve F. 3 König, Harald 3 Koutny, Maciej 3 Lang, Frédéric 3 Latella, Diego 3 Leavens, Gary T. ...and 1,306 more Authors all top 5 Fields 856 Computer science (68-XX) 92 Mathematical logic and foundations (03-XX) 53 General and overarching topics; collections (00-XX) 25 Systems theory; control (93-XX) 19 History and biography (01-XX) 11 Information and communication theory, circuits (94-XX) 10 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 9 Category theory; homological algebra (18-XX) 8 Operations research, mathematical programming (90-XX) 5 Probability theory and stochastic processes (60-XX) 5 Numerical analysis (65-XX) 5 Biology and other natural sciences (92-XX) 4 Order, lattices, ordered algebraic structures (06-XX) 3 Linear and multilinear algebra; matrix theory (15-XX) 3 Mathematics education (97-XX) 2 Combinatorics (05-XX) 2 General algebraic systems (08-XX) 2 Statistics (62-XX) 1 Associative rings and algebras (16-XX) 1 Measure and integration (28-XX) 1 Ordinary differential equations (34-XX) 1 Mechanics of particles and systems (70-XX) 1 Optics, electromagnetic theory (78-XX) 1 Quantum theory (81-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 556 Publications have been cited 3,113 times in 2,299 Documents Cited by ▼ Year ▼ A logic for reasoning about time and reliability. Zbl 0820.68113 Hansson, Hans; Jonsson, Bengt 180 1994 A new approach to abstract syntax with variable binding. Zbl 1001.68083 Gabbay, Murdoch J.; Pitts, Andrew M. 140 2002 Real time process algebra. Zbl 0719.68020 Baeten, J. C. M.; Bergstra, J. A. 59 1991 Institution morphisms. Zbl 1001.68019 Goguen, Joseph; Roşu, Grigore 51 2002 Inductive families. Zbl 0808.03044 Dybjer, Peter 45 1994 A UTP semantics for Circus. Zbl 1165.68048 Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim 38 2009 Testing equivalence as a bisimulation equivalence. Zbl 0797.68058 Cleaveland, Rance; Hennessy, Matthew 32 1993 A theory of processes with localities. Zbl 0806.68070 Boudol, G.; Castellani, I.; Hennessy, M.; Kiehn, A. 29 1994 A refinement strategy for Circus. Zbl 1093.68555 Cavalcanti, Ana; Sampaio, Augusto; Woodcock, Jim 28 2003 Safety, liveness and fairness in temporal logic. Zbl 0820.68077 Prasad Sistla, A. 27 1994 Formal aspects of correctness and optimality of interval computations. Zbl 1104.65045 Santiago, Regivan H. Nunes; Bedregal, Benjamín R. Callejas; Acióly, Benedito Melo 26 2006 Soundness of workflow nets: classification, decidability, and analysis. Zbl 1225.68129 van der Aalst, W. M. P.; van Hee, K. M.; ter Hofstede, A. H. M.; Sidorova, N.; Verbeek, H. M. W.; Voorhoeve, M.; Wynn, M. T. 26 2011 Variations on algebra: Monadicity and generalisations of equational theories. Zbl 1004.18005 Robinson, Edmund 25 2002 Duration calculus: Logical foundations. Zbl 0887.68101 Hansen, Michael R.; Chaochen, Zhou 22 1997 Processes with probabilities, priority and time. Zbl 0820.68072 Tofts, Chris 22 1994 Discrete time process algebra. Zbl 0849.68033 Baeten, J. C. M.; Bergstra, J. A. 21 1996 The ASM refinement method. Zbl 1093.68601 Börger, Egon 21 2003 Distributing finite automata through Petri net synthesis. Zbl 1017.68062 Badouel, Éric; Caillaud, Benoît; Darondeau, P. 21 2002 Parametric probabilistic transition systems for system design and analysis. Zbl 1111.68084 Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Troina, Angelo 20 2007 Generalised folds for nested datatypes. Zbl 0937.68027 Bird, Richard; Paterson, Ross 20 1999 Winskel is (almost) right: Towards a mechanized semantics textbook. Zbl 0910.68138 Nipkow, Tobias 20 1998 Relational concurrent refinement. Zbl 1093.68061 Derrick, John; Boiten, Eerke 20 2003 Hoare logic and auxiliary variables. Zbl 0978.03026 Kleymann, Thomas 19 1999 Deciding bisimilarity is P-complete. Zbl 0758.68033 Balcázar, José; Gabarró, Joaquim; Sántha, Miklós 19 1992 Exploring probabilistic bisimulations. I. Zbl 1259.68153 Hennessy, Matthew 19 2012 A calculus and logic of resources and processes. Zbl 1111.68086 Pym, David; Tofts, Chris 18 2006 Issues in the design of a parallel object-oriented language. Zbl 0694.68012 America, Pierre 18 1989 A singleton failures semantics for communicating sequential processes. Zbl 1110.68067 Bolton, Christie; Davies, Jim 17 2006 Context induction: A proof principle for behavioural abstractions and algebraic implementations. Zbl 0739.68060 Hennicker, Rolf 17 1991 Refinement-oriented probability for CSP. Zbl 0862.68050 Morgan, Carroll; McIver, Annabelle; Seidel, Karen; Sanders, J. W. 17 1996 The Rely-Guarantee method for verifying shared variable concurrent programs. Zbl 0874.68202 Xu, Qiwen; de Roever, Willem-Paul; He, Jifeng 17 1997 A single complete rule for data refinement. Zbl 0774.68081 Gardiner, P. H. B.; Morgan, Carroll 17 1993 A process algebraic framework for specification and validation of real-time systems. Zbl 1214.68224 Sherif, Adnan; Cavalcanti, Ana; Jifeng, He; Sampaio, Augusto 16 2010 Almost ASAP semantics: from timed models to timed implementations. Zbl 1101.68670 De Wulf, Martin; Doyen, Laurent; Raskin, Jean-François 16 2005 Compositional minimisation of finite state systems using interface specifications. Zbl 0860.68067 Graf, Susanne; Steffen, Bernhard; Lüttgen, Gerald 16 1996 Property-directed incremental invariant generation. Zbl 1149.68402 Bradley, Aaron R.; Manna, Zohar 16 2008 Not necessarily closed convex polyhedra and the double description method. Zbl 1101.68674 Bagnara, Roberto; Hill, Patricia M.; Zaffanella, Enea 15 2005 Automated analysis of mutual exclusion algorithms using CCS. Zbl 0696.68039 Walker, D. J. 15 1989 Event fairness and non-interleaving concurrency. Zbl 0696.68092 Kwiatkowska, Marta Z. 15 1989 Eliminating the substitution axiom from UNITY logic. Zbl 0715.68059 Sanders, Beverly A. 15 1991 Paramorphisms. Zbl 0754.68086 Meertens, Lambert 15 1992 Proof systems for message-passing process algebras. Zbl 0857.68040 Hennessy, M.; Lin, H. 15 1996 Active learning for extended finite state machines. Zbl 1342.68174 Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard 15 2016 Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Zbl 0966.68124 Latella, Diego; Majzik, Istvan; Massink, Mieke 14 1999 CSP theorems for communicating B machines. Zbl 1103.68599 Schneider, Steve; Treharne, Helen 14 2005 A proof system for communicating processes with value-passing. Zbl 0736.68057 Hennessy, M. 14 1991 Capture-avoiding substitution as a nominal algebra. Zbl 1152.68025 Gabbay, Murdoch J.; Mathijssen, Aad 14 2008 Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter. Zbl 1519.68143 Tran, Hoang-Dung; Pal, Neelanjana; Manzanas Lopez, Diego; Musau, Patrick; Yang, Xiaodong; Nguyen, Luan Viet; Xiang, Weiming; Bak, Stanley; Johnson, Taylor T. 14 2021 Essential concepts of algebraic specification and program development. Zbl 0887.68070 Sannella, Donald; Tarlecki, Andrzej 13 1997 Process simulation and refinement. Zbl 0696.68099 Jifeng, He 13 1989 Temporal theories as modularisation units for concurrent system specification. Zbl 0746.68031 Fiadeiro, J.; Maibaum, T. 13 1992 A static view of localities. Zbl 0806.68069 Aceto, Luca 13 1994 Specification and verification challenges for sequential object-oriented programs. Zbl 1121.68074 Leavens, Gary T.; Leino, K. Rustan M.; Müller, Peter 12 2007 Graph transformation units with interleaving semantics. Zbl 0966.68114 Kreowski, Hans-Jörg; Kuske, Sabine 12 1999 Compositional failure-based semantic models for basic LOTOS. Zbl 0838.68076 Valmari, Antti; Tienari, Martti 12 1995 Do-it-yourself type theory. Zbl 0697.68020 Backhouse, Roland; Chisholm, Paul; Malcolm, Grant; Saaman, Erik 12 1989 Balancing expressiveness in formal approaches to concurrency. Zbl 1343.68171 Jones, Cliff B.; Hayes, Ian J.; Colvin, Robert J. 12 2015 Superposition refinement of reactive systems. Zbl 0852.68008 Back, R. J. R.; Sere, K. 11 1996 ZRC – A refinement calculus for \(Z\). Zbl 0934.68062 Cavalcanti, Ana; Woodcock, Jim 11 1998 ArcAngel: a tactic language for refinement. Zbl 1093.68565 Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim 11 2003 On the lattice of specifications: Applications to a specification methodology. Zbl 0782.68077 Boudriga, Noureddine; Elloumi, Fathi; Mili, Ali 11 1992 Bisimulations in calculi modelling membranes. Zbl 1152.68035 Barbuti, Roberto; Maggiolo-Schettini, Andrea; Milazzo, Paolo; Troina, Angelo 11 2008 Probabilistic verification of Herman’s self-stabilisation algorithm. Zbl 1259.68130 Kwiatkowska, Marta; Norman, Gethin; Parker, David 11 2012 A mini challenge: build a verifiable filesystem. Zbl 1123.68336 Joshi, Rajeev; Holzmann, Gerard J. 10 2007 From control law diagrams to Ada via Circus. Zbl 1226.68028 Cavalcanti, Ana; Clayton, Phil; O’Halloran, Colin 10 2011 Invariant based programming: Basic approach and teaching experiences. Zbl 1178.68334 Back, Ralph-Johan 10 2009 csp2B: A practical approach to combining CSP and B. Zbl 0969.68578 Butler, Michael 10 2000 An algebraic verification of a mobile network. Zbl 0782.68081 Orava, Fredrik; Parrow, Joachim 10 1992 Process algebra with guards: Combining hoare logic with process algebra. Zbl 0806.68078 Groote, Jan Friso; Ponse, Alban 10 1994 Thread algebra for strategic interleaving. Zbl 1131.68067 Bergstra, J. A.; Middelburg, C. A. 10 2007 Towards formally specifying and verifying transactional memory. Zbl 1298.68168 Doherty, Simon; Groves, Lindsay; Luchangco, Victor; Moir, Mark 10 2013 Timed runtime monitoring for multiparty conversations. Zbl 1375.68030 Neykova, Rumyana; Bocchi, Laura; Yoshida, Nobuko 10 2017 Building program construction and verification tools from algebraic principles. Zbl 1342.68066 Armstrong, Alasdair; Gomes, Victor B. F.; Struth, Georg 10 2016 A refinement calculus for shared-variable parallel and distributed programming. Zbl 1029.68034 Dingel, J. 10 2002 Towards a linear algebra of programming. Zbl 1259.68135 Oliveira, José N. 10 2012 Automatizing parametric reasoning on distributed concurrent systems. Zbl 0829.68052 Inverardi, Paola; Priami, Corrado; Yankelevich, Daniel 9 1994 Interpreting message flow graphs. Zbl 0838.68075 Ladkin, Peter B.; Leue, Stefan 9 1995 Testing methods for X-machines: a review. Zbl 1103.68461 Bogdanov, K.; Holcombe, M.; Ipate, F.; Seed, L.; Vanak, S. 9 2006 Angelic nondeterminism in the unifying theories of programming. Zbl 1105.68012 Cavalcanti, Ana; Woodcock, Jim; Dunne, Steve 9 2006 Responsiveness of interoperating components. Zbl 1061.68107 Reed, J. N.; Sinclair, J. E.; Roscoe, A. W. 9 2004 TIC: a tImed calculus. Zbl 0797.68059 Quemada, Juan; de Frutos, David; Azcorra, Arturo 9 1993 Recursion induction for real-time processes. Zbl 0806.68073 Davies, Jim; Schneider, Steve 9 1993 Operational semantics of resolution and productivity in Horn clause logic. Zbl 1362.68048 Fu, Peng; Komendantskaya, Ekaterina 9 2017 Probabilistic model checking of deadline properties in the IEEE 1394 fireWire root contention protocol. Zbl 1029.68017 Kwiatkowska, Marta; Norman, Gethin; Sproston, Jeremy 9 2002 Architectural specifications in CASL. Zbl 1001.68078 Bidoit, Michel; Sannella, Donald; Tarlecki, Andrzej 9 2002 From LCF to Isabelle/HOL. Zbl 1427.68349 Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius 9 2019 Specification of communicating processes: temporal logic versus refusals-based refinement. Zbl 1149.68056 Lowe, Gavin 8 2008 MetateM: An introduction. Zbl 0838.68014 Barringer, H.; Fisher, M.; Gabbay, D.; Gough, G.; Owens, R. 8 1995 Generating test sets from non-deterministic stream X-machines. Zbl 1013.68105 Ipate, Florentin; Holcombe, Mike 8 2000 A program refinement tool. Zbl 0910.68050 Carrington, D.; Hayes, I.; Nickson, R.; Watson, G.; Welsh, J. 8 1998 Verification of a sliding window protocol in \(\mu\) CRL and PVS. Zbl 1101.68309 Badban, Bahareh; Fokkink, Wan; Groote, Jan Friso; Pang, Jun; van de Pol, Jaco 8 2005 Compositional action system refinement. Zbl 1093.68007 Back, R. J. R.; von Wright, J. 8 2003 Partial order behaviour and structure of Petri nets. Zbl 0697.68061 Best, Eike; Desel, Jörg 8 1990 Refinement concepts formalised in higher order logic. Zbl 0703.68074 Back, R. J. R.; von Wright, J. 8 1990 A tactic calculus. — Abridged version. Zbl 0857.68094 Martin, A. P.; Gardiner, P. H. B.; Woodcock, J. C. P. 8 1996 Real space process algebra. Zbl 0942.68607 Baeten, J. C. M.; Bergstra, J. A. 8 1993 On sequential composition, action prefixes and process prefix. Zbl 0942.68608 Baeten, J. C. M.; Bergstra, J. A. 8 1994 A mechanically verified incremental garbage collector. Zbl 0941.68624 Russinoff, David M. 8 1994 Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. Zbl 1348.68213 Aransay, Jesús; Divasón, Jose 8 2016 Fun with fireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol. Zbl 1029.68022 Stoelinga, Mariëlle 8 2002 Algebra-based reasoning for loop synthesis. Zbl 1522.68155 Humenberger, Andreas; Amrollahi, Daneshvar; Bjørner, Nikolaj; Kovács, Laura 2 2022 Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter. Zbl 1519.68143 Tran, Hoang-Dung; Pal, Neelanjana; Manzanas Lopez, Diego; Musau, Patrick; Yang, Xiaodong; Nguyen, Luan Viet; Xiang, Weiming; Bak, Stanley; Johnson, Taylor T. 14 2021 \(L^\ast\)-based learning of Markov decision processes (extended version). Zbl 1519.68106 Tappler, Martin; Aichernig, Bernhard K.; Bacci, Giovanni; Eichlseder, Maria; Larsen, Kim G. 6 2021 Comprehensive systems: a formal foundation for multi-model consistency management. Zbl 1522.68347 Stünkel, Patrick; König, Harald; Lamo, Yngve; Rutle, Adrian 4 2021 Verifying correctness of persistent concurrent data structures: a sound and complete method. Zbl 1519.68133 Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Wehrheim, Heike 4 2021 Denotational semantics of channel mobility in UTP-CSP. Zbl 1519.68160 Ekembe Ngondi, Gerard 4 2021 Learning safe neural network controllers with barrier certificates. Zbl 1521.93054 Zhao, Hengjun; Zeng, Xia; Chen, Taolue; Liu, Zhiming; Woodcock, Jim 3 2021 An axiomatic approach to existence and liveness for differential equations. Zbl 1519.68141 Tan, Yong Kiam; Platzer, André 3 2021 From generic partition refinement to weighted tree automata minimization. Zbl 1519.68126 Wißmann, Thorsten; Deifel, Hans-Peter; Milius, Stefan; Schröder, Lutz 3 2021 Optimal and robust controller synthesis using energy timed automata with uncertainty. Zbl 1458.93072 Bacci, Giovanni; Bouyer, Patricia; Fahrenberg, Uli; Larsen, Kim G.; Markey, Nicolas; Reynier, Pierre-Alain 3 2021 Hybrid dynamic logic institutions for event/data-based systems. Zbl 1522.68322 Hennicker, Rolf; Knapp, Alexander; Madeira, Alexandre 1 2021 A process calculus BigrTiMo of mobile systems and its formal semantics. Zbl 1511.68189 Xie, Wanling; Zhu, Huibiao; Xu, Qiwen 1 2021 Model-based safety assessment of a triple modular generator with xSAP. Zbl 1511.68149 Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Jones, David; Mattarei, Cristian 1 2021 Enhancing robustness verification for deep neural networks via symbolic propagation. Zbl 1519.68228 Yang, Pengfei; Li, Jianlin; Liu, Jiangchao; Huang, Cheng-Chao; Li, Renjue; Chen, Liqian; Huang, Xiaowei; Zhang, Lijun 1 2021 GR(1)*: GR(1) specifications extended with existential guarantees. Zbl 1519.68129 Amram, Gal; Maoz, Shahar; Pistiner, Or 1 2021 A weakness measure for GR(1) formulae. Zbl 1458.68115 Cavezza, Davide G.; Alrajeh, Dalal; György, András 1 2021 Modular verification of programs with effects and effects handlers. Zbl 1458.68119 Letan, Thomas; Régis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume 1 2021 Formalization of camera pose estimation algorithm based on Rodrigues formula. Zbl 1458.68226 Chen, Shanyan; Wang, Guohui; Li, Ximeng; Zhang, Qianying; Shi, Zhiping; Guan, Yong 1 2020 Linearizability on hardware weak memory models. Zbl 1451.68030 Smith, Graeme; Winter, Kirsten; Colvin, Robert J. 1 2020 Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation. Zbl 1451.68057 Ahmad, Waqar; Hasan, Osman; Tahar, Sofiène 1 2020 Formal verification of robotic cell injection systems up to 4-DOF using HOL Light. Zbl 1458.68220 Rashid, Adnan; Hasan, Osman 1 2020 Theoretical and practical approaches to the denotational semantics for MDESL based on UTP. Zbl 1458.68041 Sheng, Feng; Zhu, Huibiao; He, Jifeng; Yang, Zongyuan; Bowen, Jonathan P. 1 2020 From LCF to Isabelle/HOL. Zbl 1427.68349 Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius 9 2019 Bisimulation and coinduction enhancements: a historical perspective. Zbl 1427.68010 Pous, Damien; Sangiorgi, Davide 6 2019 Fifty years of Hoare’s logic. Zbl 1427.68008 Apt, Krzysztof R.; Olderog, Ernst-Rüdiger 6 2019 Interactive verification of architectural design patterns in FACTum. Zbl 1425.68273 Marmsoler, Diego; Gidey, Habtom Kashay 4 2019 Multiple model synchronization with multiary delta lenses with amendment and K-Putput. Zbl 1425.68068 Diskin, Zinovy; König, Harald; Lawford, Mark 4 2019 Automated mutual induction proof in separation logic. Zbl 1425.68382 Ta, Quang-Trung; Le, Ton Chanh; Khoo, Siau-Cheng; Chin, Wei-Ngan 4 2019 Toward automatic verification of quantum programs. Zbl 1425.68271 Ying, Mingsheng 3 2019 Finding suitable variability abstractions for lifted analysis. Zbl 1425.68067 Dimovski, Aleksandar S.; Brabrand, Claus; Wąsowski, Andrzej 3 2019 A verification-driven framework for iterative design of controllers. Zbl 1425.68262 Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo 2 2019 GPU-accelerated steady-state computation of large probabilistic Boolean networks. Zbl 1425.68121 Mizera, Andrzej; Pang, Jun; Yuan, Qixia 2 2019 Milestones from the Pure Lisp Theorem Prover to ACL2. Zbl 1427.68348 Moore, J Strother 1 2019 Formal reliability analysis of redundancy architectures. Zbl 1425.68039 Bozzano, Marco; Cimatti, Alessandro; Mattarei, Cristian 1 2019 A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Zbl 1425.68293 Hayes, Ian J.; Meinicke, Larissa A.; Winter, Kirsten; Colvin, Robert J. 1 2019 A UTP semantics for communicating processes with shared variables and its formal encoding in PVS. Zbl 1398.68373 Shi, Ling; Zhao, Yongxin; Liu, Yang; Sun, Jun; Dong, Jin Song; Qin, Shengchao 4 2018 A UTP approach for rTiMo. Zbl 1425.68304 Xie, Wanling; Xiang, Shuangqing; Zhu, Huibiao 4 2018 A formal verification technique for behavioural model-to-model transformations. Zbl 1380.68286 de Putter, Sander; Wijs, Anton 2 2018 Cut branches before looking for bugs: certifiably sound verification on relaxed slices. Zbl 1380.68127 Léchenet, Jean-Christophe; Kosmatov, Nikolai; Le Gall, Pascale 2 2018 Mechanized proofs of opacity: a comparison of two techniques. Zbl 1395.68186 Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike 2 2018 Formal analysis of the kinematic Jacobian in screw theory. Zbl 1426.70008 Shi, Zhiping; Wu, Aixuan; Yang, Xiumei; Guan, Yong; Li, Yongdong; Song, Xiaoyu 2 2018 Model-based testing of probabilistic systems. Zbl 1380.68303 Gerhold, Marcus; Stoelinga, Mariëlle 1 2018 The symbiosis of concurrency and verification: teaching and case studies. Zbl 1382.68144 Pedersen, Jan B.; Welch, Peter H. 1 2018 Timed runtime monitoring for multiparty conversations. Zbl 1375.68030 Neykova, Rumyana; Bocchi, Laura; Yoshida, Nobuko 10 2017 Operational semantics of resolution and productivity in Horn clause logic. Zbl 1362.68048 Fu, Peng; Komendantskaya, Ekaterina 9 2017 Equational formulas and pattern operations in initial order-sorted algebras. Zbl 1362.68054 Meseguer, José; Skeirik, Stephen 6 2017 Designing a semantic model for a wide-spectrum language with concurrency. Zbl 1375.68036 Colvin, Robert J.; Hayes, Ian J.; Meinicke, Larissa A. 5 2017 Birkhoff style calculi for hybrid logics. Zbl 1420.03037 Găină, Daniel 4 2017 Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation. Zbl 1377.68042 Nazarpour, Hosein; Falcone, Yliès; Bensalem, Saddek; Bozga, Marius 3 2017 Maximal incompleteness as obfuscation potency. Zbl 1355.68053 Giacobazzi, Roberto; Mastroeni, Isabella; Dalla Preda, Mila 3 2017 A verification and deployment approach for elastic component-based applications. Zbl 1377.68039 Graiet, Mohamed; Hamel, Lazhar; Mammar, Amel; Tata, Samir 2 2017 Modeling and efficient verification of wireless ad hoc networks. Zbl 1377.68028 Yousefi, Behnaz; Ghassemi, Fatemeh; Khosravi, Ramtin 2 2017 Manifest domains: analysis and description. Zbl 1358.68052 Bjørner, Dines 2 2017 Proof checking and logic programming. Zbl 1362.68056 Miller, Dale 2 2017 Proving completeness of logic programs with the cut. Zbl 1355.68033 Drabent, Włodzimierz 2 2017 A compositional modelling and verification framework for stochastic hybrid systems. Zbl 1370.68220 Wang, Shuling; Zhan, Naijun; Zhang, Lijun 2 2017 Incremental bounded model checking for embedded software. Zbl 1375.68081 Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom 1 2017 Relating trace refinement and linearizability. Zbl 1377.68151 Smith, Graeme; Winter, Kirsten 1 2017 Simulation relations for fault-tolerance. Zbl 1377.68044 Demasi, Ramiro; Castro, Pablo F.; Maibaum, Thomas S. E.; Aguirre, Nazareno 1 2017 A Maude environment for CafeOBJ. Zbl 1358.68195 Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi 1 2017 Complete model-based equivalence class testing for nondeterministic systems. Zbl 1358.68043 Huang, Wen-ling; Peleska, Jan 1 2017 Deriving bisimulation relations from path based equivalence checkers. Zbl 1358.68067 Banerjee, Kunal; Sarkar, Dipankar; Mandal, Chittaranjan 1 2017 On proving confluence modulo equivalence for Constraint Handling Rules. Zbl 1355.68050 Christiansen, Henning; Kirkeby, Maja H. 1 2017 Constraint logic programming with a relational machine. Zbl 1355.68035 Gallego Arias, Emilio Jesús; Lipton, James; Mariño, Julio 1 2017 Active learning for extended finite state machines. Zbl 1342.68174 Cassel, Sofia; Howar, Falk; Jonsson, Bengt; Steffen, Bernhard 15 2016 Building program construction and verification tools from algebraic principles. Zbl 1342.68066 Armstrong, Alasdair; Gomes, Victor B. F.; Struth, Georg 10 2016 Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. Zbl 1348.68213 Aransay, Jesús; Divasón, Jose 8 2016 Model checking Petri nets with names using data-centric dynamic systems. Zbl 1345.68236 Montali, Marco; Rivkin, Andrey 8 2016 Self-adaptation and secure information flow in multiparty communications. Zbl 1345.68232 Castellani, Ilaria; Dezani-Ciancaglini, Mariangiola; Pérez, Jorge A. 7 2016 Generalised rely-guarantee concurrency: an algebraic foundation. Zbl 1348.68035 Hayes, Ian J. 6 2016 A general framework for architecture composability. Zbl 1342.68029 Attie, Paul; Baranov, Eduard; Bliudze, Simon; Jaber, Mohamad; Sifakis, Joseph 6 2016 Reversible client/server interactions. Zbl 1345.68016 Barbanera, Franco; Dezani-Ciancaglini, Mariangiola; de’Liguoro, Ugo 5 2016 On the diversity of asynchronous communication. Zbl 1345.68022 Chevrou, Florent; Hurault, Aurélie; Quéinnec, Philippe 5 2016 Rigorous development of component-based systems using component metadata and patterns. Zbl 1348.68167 Oliveira, Marcel V. M.; Antonino, P.; Ramos, R.; Sampaio, A.; Mota, A.; Roscoe, A. W. 4 2016 Analysing sanity of requirements for avionics systems. Zbl 1335.68131 Barnat, Jiří; Bauch, Petr; Beneš, Nikola; Brim, Luboš; Beran, Jan; Kratochvíla, Tomáš 4 2016 Contract-based verification of MATLAB-style matrix programs. Zbl 1338.65116 Wiik, Jonatan; Boström, Pontus 4 2016 Dynamic role authorization in multiparty conversations. Zbl 1345.68235 Ghilezan, Silvia; Jakšić, Svetlana; Pantović, Jovanka; Pérez, Jorge A.; Torres Vieira, Hugo 4 2016 Computing maximal weak and other bisimulations. Zbl 1355.68190 Boulgakov, Alexandre; Gibson-Robinson, Thomas; Roscoe, A. W. 3 2016 A language-independent proof system for full program equivalence. Zbl 1355.68051 Ciobâcă, Ştefan; Lucanu, Dorel; Rusu, Vlad; Roşu, Grigore 3 2016 Deciding probabilistic automata weak bisimulation: theory and practice. Zbl 1335.68117 Ferrer Fioriti, Luis María; Hashemi, Vahid; Hermanns, Holger; Turrini, Andrea 2 2016 Verification of \(\mathrm{EB}^3\) specifications using CADP. Zbl 1335.68150 Vekris, Dimitris; Lang, Frédéric; Dima, Catalin; Mateescu, Radu 2 2016 Optimising the ProB model checker for B using partial order reduction. Zbl 1342.68208 Dobrikov, Ivaylo; Leuschel, Michael 2 2016 Event-based run-time adaptation in communication-centric systems. Zbl 1345.68234 Di Giusto, Cinzia; Pérez, Jorge A. 2 2016 Formalising concurrent UML state machines using coloured Petri nets. Zbl 1345.68226 André, Étienne; Benmoussa, Mohamed Mahdi; Choppy, Christine 2 2016 Foundations for using linear temporal logic in Event-B refinement. Zbl 1348.68039 Hoang, Thai Son; Schneider, Steve; Treharne, Helen; Williams, David M. 1 2016 Component-wise incremental LTL model checking. Zbl 1355.68178 Molnár, Vince; Vörös, András; Darvas, Dániel; Bartha, Tamás; Majzik, István 1 2016 A unified integration and component testing approach from deterministic stream X-machine specifications. Zbl 1335.68021 Ipate, Florentin; Dranidis, Dimitris 1 2016 Correctness and concurrent complexity of the black-white bakery algorithm. Zbl 1342.68348 Hesselink, Wim H. 1 2016 ASM-based formal design of an adaptivity component for a cloud system. Zbl 1345.68021 Arcaini, Paolo; Holom, Roxana-Maria; Riccobene, Elvinia 1 2016 On the expressive power of behavioral profiles. Zbl 1345.68237 Polyvyanyy, Artem; Armas-Cervantes, Abel; Dumas, Marlon; García-Bañuelos, Luciano 1 2016 Balancing expressiveness in formal approaches to concurrency. Zbl 1343.68171 Jones, Cliff B.; Hayes, Ian J.; Colvin, Robert J. 12 2015 A linear algebra approach to OLAP. Zbl 1331.68055 Macedo, Hugo Daniel; Oliveira, José 7 2015 Refinement in hybridised institutions. Zbl 1331.68149 Madeira, Alexandre; Martins, Manuel A.; Barbosa, Luís S.; Hennicker, Rolf 6 2015 Denotational semantics and its algebraic derivation for an event-driven system-level language. Zbl 1347.68039 Zhu, H.; He, Jifeng; Qin, Shengchao; Brooke, Phillip 5 2015 An algebraic theory for web service contracts. Zbl 1338.68016 Laneve, Cosimo; Padovani, Luca 5 2015 Compositional reasoning about active objects with shared futures. Zbl 1343.68166 Din, Crystal Chang; Owe, Olaf 4 2015 Proof-based verification approaches for dynamic properties: application to the information system domain. Zbl 1331.68142 Mammar, Amel; Frappier, Marc 4 2015 Program equivalence by circular reasoning. Zbl 1319.68060 Lucanu, Dorel; Rusu, Vlad 4 2015 Categorical foundations for structured specifications in \(\mathsf{Z}\). Zbl 1385.68023 Castro, Pablo F.; Aguirre, Nazareno; Pombo, Carlos L.; Maibaum, T. S. E. 3 2015 Verification of distributed systems with the axiomatic system of MSVL. Zbl 1328.68032 Ma, Qian; Duan, Zhenhua; Zhang, Nan; Wang, Xiaobing 3 2015 ...and 456 more Documents all cited Publications top 5 cited Publications all top 5 Cited by 2,948 Authors 34 Cavalcanti, Ana 28 Bergstra, Jan A. 27 Katoen, Joost-Pieter 27 Woodcock, James C. P. 19 Kwiatkowska, Marta Z. 17 Bedregal, Benjamín René Callejas 17 Hesselink, Wim H. 17 Middelburg, Cornelis A. 16 Derrick, John 16 Gabbay, Murdoch James 16 Larsen, Kim Guldstrand 16 Mossakowski, Till 16 Schellhorn, Gerhard 15 Baier, Christel 14 Hayes, Ian J. 13 Aceto, Luca 13 Colvin, Robert J. 13 Hennessy, Matthew C. B. 13 Legay, Axel 13 Meseguer Guaita, José 13 Wehrheim, Heike 13 Zeyda, Frank 12 Baeten, Jos C. M. 12 Diaconescu, Răzvan 12 Ingólfsdóttir, Anna 12 Power, John 12 Roscoe, Andrew William 12 van Glabbeek, Robert Jan 11 Bernardo, Marco 11 Bonchi, Filippo 11 Dybjer, Peter 11 Groote, Jan Friso 11 Guttmann, Walter 11 Hennicker, Rolf 11 Hermanns, Holger 11 Junges, Sebastian 11 Liu, Zhiming 11 Norman, Gethin 11 Roşu, Grigore 11 Tini, Simone 11 Tredup, Ronny 11 Zhu, Huibiao 10 Banach, Richard 10 Corradini, Flavio 10 Foster, Simon 10 Gibbons, Jeremy 10 Madeira, Alexandre 10 Schneider, Steve A. 10 Tarlecki, Andrzej 10 Tzevelekos, Nikos 9 Bonsangue, Marcello Maria 9 Chatterjee, Krishnendu 9 Delahaye, Benoît 9 Dezani-Ciancaglini, Mariangiola 9 Dongol, Brijesh 9 He, Jifeng 9 Hierons, Robert Mark 9 Kuske, Sabine 9 Montanari, Ugo G. 9 Ponse, Alban 9 Sangiorgi, Davide 9 Santiago, Regivan H. Nunes 9 Vaandrager, Frits W. 9 Zhang, Lijun 8 Bidoit, Michel 8 Boiten, Eerke A. 8 Börger, Egon 8 Cheney, James 8 Devillers, Raymond 8 Ipate, Florentin 8 Kreowski, Hans-Jörg 8 Kucera, Antonin 8 Kupferman, Orna 8 Luttik, Bas 8 Murawski, Andrzej S. 8 Oliveira, José Nuno 8 Peled, Doron A. 8 Pitts, Andrew M. 8 Rutten, Jan J. M. M. 8 Sannella, Donald T. 8 Schröder, Lutz 8 Silva, Alexandra 8 Smith, Graeme 8 Struth, Georg 8 Zhan, Naijun 7 Aichernig, Bernhard K. 7 Barbosa, Luís Soares 7 Best, Eike 7 Bouyer, Patricia 7 Castiglioni, Valentina 7 Degano, Pierpaolo 7 Deng, Yuxin 7 Esparza, Javier 7 Feng, Yuan 7 Fernández, Maribel 7 Ferrari, Gian Luigi 7 Forejt, Vojtěch 7 Francalanza, Adrian 7 Garavel, Hubert 7 Ghani, Neil ...and 2,848 more Authors all top 5 Cited in 124 Journals 294 Theoretical Computer Science 271 Formal Aspects of Computing 97 Information and Computation 72 Journal of Logical and Algebraic Methods in Programming 62 The Journal of Logic and Algebraic Programming 60 Acta Informatica 50 Formal Methods in System Design 46 Information Processing Letters 45 Logical Methods in Computer Science 44 Journal of Automated Reasoning 36 Science of Computer Programming 30 MSCS. Mathematical Structures in Computer Science 28 Journal of Functional Programming 20 Information Sciences 20 Annals of Pure and Applied Logic 18 Journal of Computer and System Sciences 15 Annals of Mathematics and Artificial Intelligence 15 ACM Transactions on Computational Logic 14 Distributed Computing 14 Fundamenta Informaticae 14 Theory and Practice of Logic Programming 10 Artificial Intelligence 10 Journal of Applied Logic 9 Fuzzy Sets and Systems 9 Journal of Symbolic Computation 8 The Journal of Symbolic Logic 8 International Journal of Approximate Reasoning 8 International Journal of Foundations of Computer Science 8 Journal of Applied Non-Classical Logics 7 Journal of Computer Science and Technology 7 Theory of Computing Systems 7 Logica Universalis 6 Higher-Order and Symbolic Computation 5 International Journal of Computer Mathematics 5 Frontiers of Computer Science 4 Discrete Applied Mathematics 4 Computing 4 Journal of Philosophical Logic 4 Journal of Pure and Applied Algebra 4 Programming and Computer Software 4 Studia Logica 4 Real-Time Systems 4 Discrete Event Dynamic Systems 4 Mathematical Problems in Engineering 4 RAIRO. Theoretical Informatics and Applications 4 Mathematics in Computer Science 3 Journal of Logic, Language and Information 3 Computational and Applied Mathematics 3 Journal of the ACM 3 Journal of Applied Mathematics 3 Computer Science Review 2 International Journal of General Systems 2 Automatica 2 Mathematics and Computers in Simulation 2 Synthese 2 Machine Learning 2 JETAI. Journal of Experimental & Theoretical Artificial Intelligence 2 Applied Categorical Structures 2 The Bulletin of Symbolic Logic 2 Soft Computing 2 Journal of Combinatorial Optimization 2 LMS Journal of Computation and Mathematics 2 Journal of Systems Science and Complexity 2 Sādhanā 2 Natural Computing 2 Computer Languages, Systems & Structures 2 The Review of Symbolic Logic 2 Frontiers of Computer Science in China 2 Categories and General Algebraic Structures with Applications 1 ACM Computing Surveys 1 Computers & Mathematics with Applications 1 International Journal of Control 1 Bulletin of Mathematical Biology 1 The Mathematical Intelligencer 1 Applied Mathematics and Computation 1 Journal of Optimization Theory and Applications 1 Notre Dame Journal of Formal Logic 1 Rendiconti del Circolo Matemàtico di Palermo. Serie II 1 Siberian Mathematical Journal 1 Systems & Control Letters 1 New Generation Computing 1 Algorithmica 1 International Journal of Intelligent Systems 1 Mathematical and Computer Modelling 1 Computational Geometry 1 International Journal of Algebra and Computation 1 RAIRO. Informatique Théorique et Applications 1 Archive for Mathematical Logic 1 Indagationes Mathematicae. New Series 1 Applicable Algebra in Engineering, Communication and Computing 1 Foundations of Computing and Decision Sciences 1 Experimental Mathematics 1 Journal of Computer and Systems Sciences International 1 Journal of Mathematical Sciences (New York) 1 Mathematical Logic Quarterly (MLQ) 1 The Journal of Artificial Intelligence Research (JAIR) 1 Theory and Applications of Categories 1 Complexity 1 Topoi 1 Journal of Group Theory ...and 24 more Journals all top 5 Cited in 34 Fields 2,138 Computer science (68-XX) 503 Mathematical logic and foundations (03-XX) 75 Category theory; homological algebra (18-XX) 51 Systems theory; control (93-XX) 50 Operations research, mathematical programming (90-XX) 37 Probability theory and stochastic processes (60-XX) 37 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 34 Biology and other natural sciences (92-XX) 26 Information and communication theory, circuits (94-XX) 20 Order, lattices, ordered algebraic structures (06-XX) 17 Combinatorics (05-XX) 15 General algebraic systems (08-XX) 10 Linear and multilinear algebra; matrix theory (15-XX) 10 Numerical analysis (65-XX) 9 General topology (54-XX) 8 History and biography (01-XX) 7 General and overarching topics; collections (00-XX) 7 Group theory and generalizations (20-XX) 7 Algebraic topology (55-XX) 6 Convex and discrete geometry (52-XX) 6 Quantum theory (81-XX) 6 Mathematics education (97-XX) 5 Statistics (62-XX) 4 Associative rings and algebras (16-XX) 4 Ordinary differential equations (34-XX) 3 Measure and integration (28-XX) 3 Calculus of variations and optimal control; optimization (49-XX) 2 Mechanics of particles and systems (70-XX) 1 Number theory (11-XX) 1 Commutative algebra (13-XX) 1 Real functions (26-XX) 1 Geometry (51-XX) 1 Fluid mechanics (76-XX) 1 Relativity and gravitational theory (83-XX) Citations by Year