Edit Profile (opens in new tab) Pnueli, Amir Compute Distance To: Compute Author ID: pnueli.amir Published as: Pnueli, Amir; Pnueli, A. Further Spellings: אמיר פנואלי External Links: MGP · Wikidata · dblp · GND · IdRef Awards: Turing Award (1996) Documents Indexed: 162 Publications since 1968, including 1 Book 4 Contributions as Editor · 1 Further Contribution Biographic References: 6 Publications Co-Authors: 98 Co-Authors with 153 Joint Publications 2,363 Co-Co-Authors all top 5 Co-Authors 12 single-authored 26 Zuck, Lenore D. 25 Manna, Zohar 16 Kesten, Yonit 12 Maler, Oded 9 Balaban, Ittai 8 Harel, David 8 Piterman, Nir 6 Fang, Yi 5 Kugler, Hillel 5 Stavi, Jonathan 4 Arons, Tamarah 4 Ben-Ari, Mordechai 4 Damm, Werner 4 Even, Shimon 4 Francez, Nissim 4 Nickovic, Dejan 4 Peled, Doron A. 4 Rodeh, Yoav 4 Sa’ar, Yaniv 4 Shahar, Elad 3 Asarin, Eugene 3 Lehmann, Daniel J. 3 Lempel, Abraham 3 Ruah, Sitvanit 3 Shtrichman, Ofer 3 Siegel, Michael 3 Sifakis, Joseph 3 Strichman, Ofer 2 Apt, Krzysztof Rafal 2 Ashcroft, Edward A. 2 Barrett, Clark W. 2 Barringer, Howard 2 Cohen, Ariel 2 Goldberg, Benjamin 2 Halpern, Joseph Yehuda 2 Hart, Sergiu 2 Henzinger, Thomas A. 2 Hu, Ying 2 Hubbard, E. Jane Albert 2 Josko, Bernhard 2 Klein, Uri 2 Lichtenstein, Orna 2 Marelly, Rami 2 Mysore, Venkatesh P. 2 Pekeris, Chaim Leib 2 Prywes, Noah S. 2 Rosner, Roni 2 Sharir, Micha 2 Slutzki, Giora 2 Stern, Michael J. 2 Vardi, Moshe Ya’akov 2 Votintseva, Angelika 1 Banieqbal, Behnam 1 Bloem, Roderick 1 Bontemps, Yves 1 Bournez, Olivier 1 Boyer, Robert S. 1 Burstall, Rod M. 1 Cohen, Shimon 1 Commoner, F. G. 1 Dierks, Henning 1 Dijkstra, Edsger Wybe 1 Fisman, Dana 1 Gabbay, Dov M. 1 Goguen, Joseph Amadee 1 Gordin, I. V. 1 Grumberg, Orna 1 Harel, Eyal 1 Holt, Anatol W. 1 Jobstmann, Barbara 1 Kam, Na’aman 1 Kaplan, Stéphane 1 Katz, Shmuel 1 Keste, Y. 1 Klebansky, Boris 1 Koren, Tmima 1 Kuiper, Ruurd 1 Kupferman, Orna 1 Langberg, Michael 1 Leung, Allen Yuk Lun 1 Leviathan, R. 1 Lu, Yuan 1 McMillan, Kenneth L. 1 Moore, J Strother 1 Niebert, Peter 1 Oehlerking, Jens 1 Olshansky, Tmima 1 Palem, Krishna V. 1 Podelski, Andreas 1 Raviv, Li-On 1 Ron, Dorit 1 Rosemberg, Flavia 1 Rybalchenko, Andrey 1 Schneider, Gerardo 1 Sedletsky, Ekaterina 1 Shalev, Matan 1 Sinha, Nishant 1 Talupur, Muralidhar 1 Virbitskaite, Irina B. 1 Voronkov, Andrei ...and 4 more Co-Authors all top 5 Serials 11 Theoretical Computer Science 9 Information and Computation 7 Journal of Computer and System Sciences 6 Acta Informatica 3 Journal of the Association for Computing Machinery 3 SIAM Journal on Computing 3 Lecture Notes in Computer Science 2 ACM Transactions on Programming Languages and Systems 2 Science of Computer Programming 2 Formal Methods in System Design 2 Logic Journal of the IGPL 2 1 Canadian Journal of Mathematics 1 Philosophical Transactions of the Royal Society of London. Ser. A 1 Journal of Logic and Computation 1 International Journal of Foundations of Computer Science 1 IEEE Transactions on Software Engineering 1 Proceedings of the Royal Society of London. Series A. Mathematical and Physical Sciences 1 Distributed Computing 1 Constraints 1 Computer Languages, Systems & Structures all top 5 Fields 158 Computer science (68-XX) 45 Mathematical logic and foundations (03-XX) 7 Systems theory; control (93-XX) 3 General and overarching topics; collections (00-XX) 3 Information and communication theory, circuits (94-XX) 2 Combinatorics (05-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Biology and other natural sciences (92-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Convex and discrete geometry (52-XX) 1 Statistics (62-XX) 1 Numerical analysis (65-XX) 1 Operations research, mathematical programming (90-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 148 Publications have been cited 2,155 times in 1,569 Documents Cited by ▼ Year ▼ The temporal logic of reactive and concurrent systems. Specification. Zbl 0753.68003Manna, Zohar; Pnueli, Amir 194 1991 On the synthesis of an asynchronous reactive module. Zbl 0686.68015Pnueli, Amir; Rosner, Roni 172 1989 Transitive orientation of graphs and identification of permutation graphs. Zbl 0204.24604Pnueli, A.; Lempel, A.; Even, S. 99 1971 Marked directed graphs. Zbl 0238.05109Commoner, F.; Holt, A. W.; Even, S.; Pnueli, A. 94 1971 The temporal semantics of concurrent programs. Zbl 0441.68010Pnueli, Amir 75 1981 On the synthesis of discrete controllers for timed systems. Zbl 1379.68227Maler, Oded; Pnueli, Amir; Sifakis, Joseph 70 1995 Impartiality, justice and fairness: The ethics of concurrent termination. Zbl 0468.68026Lehmann, D.; Pnueli, A.; Stavi, J. 65 1981 Reachability analysis of dynamical systems having piecewise-constant derivatives. Zbl 0884.68050Asarin, Eugene; Maler, Oded; Pnueli, Amir 53 1995 Permutation graphs and transitive graphs. Zbl 0251.05113Even, S.; Pnueli, A.; Lempel, A. 50 1972 The temporal logic of branching time. Zbl 0533.68036Ben-Ari, Mordechai; Pnueli, Amir; Manna, Zohar 49 1983 Temporal verification of reactive systems: response. Zbl 1288.68169Manna, Zohar; Pnueli, Amir 46 2010 Synthesis of Reactive(1) designs. Zbl 1247.68050Bloem, Roderick; Jobstmann, Barbara; Piterman, Nir; Pnueli, Amir; Sa’ar, Yaniv 44 2012 The glory of the past. Zbl 0586.68028Lichtenstein, Orna; Pnueli, Amir; Zuck, Lenore 41 1985 On the development of reactive systems. Zbl 0581.68046Harel, D.; Pnueli, A. 40 1985 Symbolic model checking with rich assertional languages. Zbl 0973.68119Kesten, Y.; Maler, O.; Marcus, M.; Pnueli, A.; Shahar, E. 33 2001 Termination of probabilistic concurrent programs. Zbl 0511.68009Hart, Sergiu; Sharir, Micha; Pnueli, Amir 31 1983 Synthesis of reactive(1) designs. Zbl 1176.68126Piterman, Nir; Pnueli, Amir; Sa’ar, Yaniv 30 2006 Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. Zbl 0607.68022Pnueli, A. 29 1986 Propositional temporal logics: Decidability and completeness. Zbl 1033.03009Lichtenstein, Orna; Pnueli, Amir 28 2000 Completing the temporal picture. Zbl 0795.68133Manna, Zohar; Pnueli, Amir 26 1991 Verification of parameterized programs. Zbl 0844.68079Manna, Zohar; Pnueli, Amir 26 1995 The anchored version of the temporal framework. (Tutorial). Zbl 0683.68031Manna, Z.; Pnueli, A. 25 1989 Propositional dynamic logic of nonregular programs. Zbl 0536.68041Harel, David; Pnueli, Amir; Stavi, Jonathan 23 1983 Verification of multiprocess probabilistic protocols. Zbl 0598.68019Pnueli, Amir; Zuck, Lenore 21 1986 Adequate proof principles for invariance and liveness properties of concurrent programs. Zbl 0542.68014Manna, Zohar; Pnueli, Amir 20 1984 Formalization of properties of functional programs. Zbl 0206.17503Manna, Zohar; Pnueli, Amir 19 1970 Automatic deductive verification with invisible invariants. Zbl 0978.68539Pnueli, Amir; Ruah, Sitvanit; Zuck, Lenore 19 2001 On the learnability of infinitary regular sets. Zbl 0834.68099Maler, Oded; Pnueli, Amir 19 1995 On discretization of delays in timed automata and digital circuits. Zbl 0933.94045Asarin, Eugene; Maler, Oded; Pnueli, Amir 19 1998 Decidable properties of monadic functional schemas. Zbl 0289.68036Ashcroft, Edward; Manna, Zohar; Pnueli, Amir 18 1973 Verification by augmented finitary abstraction. Zbl 1003.68069Kesten, Yonit; Pnueli, Amir 18 2000 Liveness with \({(0,1,\infty)}\)-counter abstraction. Zbl 1010.68095Pnueli, Amir; Xu, Jessie; Zuck, Lenore 17 2002 Linear and branching structures in the semantics and logics of reactive systems. Zbl 0575.68042Pnueli, Amir 16 1985 A linear-history semantics for languages for distributed programming. Zbl 0543.68019Francez, N.; Lehmann, D.; Pnueli, A. 16 1984 Parameterized verification with automatically computed inductive assertions. Zbl 0991.68541Arons, Tamarah; Pnueli, Amir; Ruah, Sitvanit; Xu, Ying; Zuck, Lenore 15 2001 Real time temporal logic: Past, present, future. Zbl 1175.03009Maler, Oded; Nickovic, Dejan; Pnueli, Amir 15 2005 Models for reactivity. Zbl 0790.68041Manna, Zohar; Pnueli, Amir 15 1993 Temporal proof methodologies for timed transition systems. Zbl 0820.68085Henzinger, Thomas A.; Manna, Zohar; Pnueli, Amir 15 1994 Deterministic propositional dynamic logic: finite models, complexity, and completeness. Zbl 0512.03013Ben-Ari, Mordechai; Halpern, Joseph Y.; Pnueli, Amir 15 1982 Decidable integration graphs. Zbl 1045.68566Kesten, Y.; Pnueli, A.; Sifakis, J.; Yovine, S. 14 1999 In transition from global to modular temporal reasoning about programs. Zbl 0578.68014Pnueli, Amir 14 1985 From MITL to timed automata. Zbl 1141.68436Maler, Oded; Nickovic, Dejan; Pnueli, Amir 14 2006 Liveness and acceleration in parameterized verification. Zbl 0974.68521Pnueli, Amir; Shahar, Elad 12 2000 Complete proof system for QPTL. Zbl 1013.03012Kesten, Yonit; Pnueli, Amir 12 2002 Deciding equality formulas by small domains instantiations. Zbl 1046.68605Pnueli, Amir; Rodeh, Yoav; Shtrichman, Ofer; Siegel, Michael 12 1999 Probabilistic verification. Zbl 0797.68112Pnueli, Amir; Zuck, Lenore D. 12 1993 A direct algorithm for checking equivalence of LL(k) grammars. Zbl 0358.68118Olshansky, Tmima; Pnueli, Amir 11 1977 The temporal semantics of concurrent programs. Zbl 0402.68009Pnueli, Amir 11 1979 Control and data abstraction: The cornerstones of practical formal verification. Zbl 1059.68589Kesten, Yonit; Pnueli, Amir 11 2000 Checking temporal properties of discrete, timed and continuous behaviors. Zbl 1133.68378Maler, Oded; Nickovic, Dejan; Pnueli, Amir 11 2008 Verification of concurrent programs: temporal proof principles. Zbl 0481.68019Manna, Zohar; Pnueli, Amir 11 1982 Verification of concurrent programs: A temporal proof system. Zbl 0507.68005Manna, Zohar; Pnueli, Amir 11 1983 Axiomatic approach to total correctness of programs. Zbl 0263.68009Manna, Zohar; Pnueli, Amir 10 1974 Model checking and abstraction to the aid of parameterized systems (a survey). Zbl 1072.68069Zuck, Lenore; Pnueli, Amir 10 2004 A compositional approach to CTL\(^*\) verification. Zbl 1079.68059Kesten, Yonit; Pnueli, Amir 10 2005 Proving partial order properties. Zbl 0803.68070Peled, Doron; Pnueli, Amir 10 1994 A deductive proof system for CTL\(^{\ast}\). Zbl 1012.68119Pnueli, Amir; Kesten, Yonit 9 2002 TVOC: A translation validator for optimizing compilers. Zbl 1081.68606Barrett, Clark; Fang, Yi; Goldberg, Benjamin; Hu, Ying; Pnueli, Amir; Zuck, Lenore 9 2005 The code validation tool (CVT). Automatic verification of a compilation process. Zbl 1022.68733Pnueli, A.; Shtrichman, O.; Siegel, M. 9 1998 Once and for all. Zbl 1245.03022Kupferman, Orna; Pnueli, Amir; Vardi, Moshe Y. 9 2012 Smart play-out of behavioral requirements. Zbl 1019.68622Harel, David; Kugler, Hillel; Marelly, Rami; Pnueli, Amir 9 2002 Fair termination revisited - with delay. Zbl 0542.68015Apt, Krysztof R.; Pnueli, A.; Stavi, J. 9 1984 Temporal logic and fair discrete systems. Zbl 1392.68263Piterman, Nir; Pnueli, Amir 8 2018 From falsification to verification. Zbl 1052.68086Peled, Doron; Pnueli, Amir; Zuck, Lenore 8 2001 On the merits of temporal testers. Zbl 1143.68046Pnueli, A.; Zaks, A. 8 2008 Verification of probabilistic programs. Zbl 0533.68012Sharir, Micha; Pnueli, Amir; Hart, Sergiu 8 1984 Temporal logic for scenario-based specifications. Zbl 1087.68596Kugler, Hillel; Harel, David; Pnueli, Amir; Lu, Yuan; Bontemps, Yves 7 2005 Temporal verification diagrams. Zbl 0942.03527Manna, Zohar; Pnueli, Amir 7 1994 The small model property: How small can it be? Zbl 1012.03040Pnueli, Amir; Rodeh, Yoav; Strichman, Ofer; Siegel, Michael 7 2002 Orthogonal polyhedra: Representation and computation. Zbl 0947.68154Bournez, Olivier; Maler, Oded; Pnueli, Amir 7 1999 Synthesis revisited: Generating statechart models from scenario-based requirements. Zbl 1075.68614Harel, David; Kugler, Hillel; Pnueli, Amir 7 2005 A compositional temporal approach to a CSP-like language. Zbl 0594.68018Barringer, Howard; Kuiper, Ruurd; Pnueli, Amir 7 1986 Completing the temporal picture. Zbl 0703.68075Manna, Zohar; Pnueli, Amir 7 1989 Special issue on Hybrid systems. Zbl 0879.00023 6 1995 Low dimensional hybrid systems – decidable, undecidable, don’t know. Zbl 1279.68127Asarin, Eugene; Mysore, Venkatesh P.; Pnueli, Amir; Schneider, Gerardo 6 2012 Proving partial order liveness properties. Zbl 0765.68137Peled, Doron; Pnueli, Amir 6 1990 Formal modeling of C. elegans development: A scenario-based approach. Zbl 1053.92034Kam, Na’aman; Harel, David; Kugler, Hillel; Marelly, Rami; Pnueli, Amir; Hubbard, E. Jane Albert; Stern, Michael J. 6 2003 On synthesizing controllers from bounded-response properties. Zbl 1135.68477Maler, Oded; Nickovic, Dejan; Pnueli, Amir 6 2007 The modal logic of programs. Zbl 0404.68011Manna, Zohar; Pnueli, Amir 5 1979 Model checking with strong fairness. Zbl 1100.68066Kesten, Yonit; Pnueli, Amir; Raviv, Li-On; Shahar, Elad 5 2006 Beyond regular model checking. Zbl 1052.68084Fisman, Dana; Pnueli, Amir 5 2001 Shape analysis by predicate abstraction. Zbl 1111.68396Balaban, Ittai; Pnueli, Amir; Zuck, Lenore D. 5 2005 Parameterized verification by probabilistic abstraction. Zbl 1029.68104Arons, Tamarah; Pnueli, Amir; Zuck, Lenore 5 2003 Applications of temporal logic to the specification of real time systems. Zbl 0688.68024Pnueli, Amir; Harel, Eyal 5 1988 There exist decidable context free propositional dynamic logics. Zbl 0542.68020Koren, Tmima; Pnueli, Amir 5 1984 A proof method for cyclic programs. Zbl 0367.68009Francez, Nissim; Pnueli, Amir 4 1978 Network invariants in action. Zbl 1012.68131Kesten, Yonit; Pnueli, Amir; Shahar, Elad; Zuck, Lenore 4 2002 System specification and refinement in temporal logic. Zbl 0919.03027Pnueli, Amir 4 1992 Symmetric and economical solutions to the mutual exclusion problem in a distributed system. Zbl 0985.68509Cohen, Shimon; Lehmann, Daniel; Pnueli, Amir 4 1984 Is the interesting part of process logic uninteresting?: A translation from PL to PDL. Zbl 0551.68031Sherman, R.; Pnueli, A.; Harel, D. 4 1984 Simple programs and their decision problems. Zbl 0364.68014Pnueli, A.; Slutzki, G. 3 1977 Decidable properties of monadic functional schemas. Zbl 0306.68048Ashcroft, E.; Manna, Z.; Pnueli, A. 3 1971 A sound and complete deductive system for CTL\(^*\) verification. Zbl 1156.68036Gabbay, Dov M.; Pnueli, Amir 3 2008 Range allocation for equivalence logic. Zbl 1052.68088Pnueli, Amir; Rodeh, Yoav; Shtrichman, Ofer 3 2001 Effective synthesis of asynchronous systems from GR(1) specifications. Zbl 1326.68186Klein, Uri; Piterman, Nir; Pnueli, Amir 3 2012 Towards component based design of hybrid systems: safety and stability. Zbl 1288.68162Damm, Werner; Dierks, Henning; Oehlerking, Jens; Pnueli, Amir 3 2010 A discrete-time UML semantics for concurrency and communication in safety-critical applications. Zbl 1075.68048Damm, Werner; Josko, Bernhard; Pnueli, Amir; Votintseva, Angelika 3 2005 Bridging the gap between fair simulation and trace inclusion. Zbl 1082.68055Kesten, Yonit; Piterman, Nir; Pnueli, Amir 3 2005 tlpvs: A pvs-based ltl verification system. Zbl 1274.68202Pnueli, Amir; Arons, Tamarah 3 2003 Hybrid systems: computation and control. 6th international workshop, HSCC 2003, Prague, Czech Republic, April 3–5, 2003. Proceedings. Zbl 1017.00053 3 2003 Temporal logic and fair discrete systems. Zbl 1392.68263Piterman, Nir; Pnueli, Amir 8 2018 Synthesis of Reactive(1) designs. Zbl 1247.68050Bloem, Roderick; Jobstmann, Barbara; Piterman, Nir; Pnueli, Amir; Sa’ar, Yaniv 44 2012 Once and for all. Zbl 1245.03022Kupferman, Orna; Pnueli, Amir; Vardi, Moshe Y. 9 2012 Low dimensional hybrid systems – decidable, undecidable, don’t know. Zbl 1279.68127Asarin, Eugene; Mysore, Venkatesh P.; Pnueli, Amir; Schneider, Gerardo 6 2012 Effective synthesis of asynchronous systems from GR(1) specifications. Zbl 1326.68186Klein, Uri; Piterman, Nir; Pnueli, Amir 3 2012 Revisiting synthesis of GR(1) specifications. Zbl 1325.68151Klein, Uri; Pnueli, Amir 2 2011 Temporal verification of reactive systems: response. Zbl 1288.68169Manna, Zohar; Pnueli, Amir 46 2010 Towards component based design of hybrid systems: safety and stability. Zbl 1288.68162Damm, Werner; Dierks, Henning; Oehlerking, Jens; Pnueli, Amir 3 2010 Checking temporal properties of discrete, timed and continuous behaviors. Zbl 1133.68378Maler, Oded; Nickovic, Dejan; Pnueli, Amir 11 2008 On the merits of temporal testers. Zbl 1143.68046Pnueli, A.; Zaks, A. 8 2008 A sound and complete deductive system for CTL\(^*\) verification. Zbl 1156.68036Gabbay, Dov M.; Pnueli, Amir 3 2008 All you need is compassion. Zbl 1138.68457Pnueli, Amir; Sa’ar, Yaniv 3 2008 Mechanical verification of transactional memories with non-transactional memory accesses. Zbl 1155.68430Cohen, Ariel; Pnueli, Amir; Zuck, Lenore D. 3 2008 Discriminative model checking. Zbl 1155.68444Niebert, Peter; Peled, Doron; Pnueli, Amir 2 2008 On synthesizing controllers from bounded-response properties. Zbl 1135.68477Maler, Oded; Nickovic, Dejan; Pnueli, Amir 6 2007 Shape analysis of single-parent heaps. Zbl 1132.68346Balaban, Ittai; Pnueli, Amir; Zuck, Lenore D. 3 2007 Modular ranking abstraction. Zbl 1109.68062Balaban, Ittai; Pnueli, Amir; Zuck, Lenore D. 2 2007 Synthesis of reactive(1) designs. Zbl 1176.68126Piterman, Nir; Pnueli, Amir; Sa’ar, Yaniv 30 2006 From MITL to timed automata. Zbl 1141.68436Maler, Oded; Nickovic, Dejan; Pnueli, Amir 14 2006 Model checking with strong fairness. Zbl 1100.68066Kesten, Yonit; Pnueli, Amir; Raviv, Li-On; Shahar, Elad 5 2006 Ranking abstraction of recursive programs. Zbl 1176.68047Balaban, Ittai; Cohen, Ariel; Pnueli, Amir 2 2006 Reduced functional consistency of uninterpreted functions. Zbl 1272.03071Pnueli, Amir; Strichman, Ofer 2 2006 Liveness by invisible invariants. Zbl 1225.68114Fang, Yi; McMillan, Kenneth L.; Pnueli, Amir; Zuck, Lenore D. 1 2006 Real time temporal logic: Past, present, future. Zbl 1175.03009Maler, Oded; Nickovic, Dejan; Pnueli, Amir 15 2005 A compositional approach to CTL\(^*\) verification. Zbl 1079.68059Kesten, Yonit; Pnueli, Amir 10 2005 TVOC: A translation validator for optimizing compilers. Zbl 1081.68606Barrett, Clark; Fang, Yi; Goldberg, Benjamin; Hu, Ying; Pnueli, Amir; Zuck, Lenore 9 2005 Temporal logic for scenario-based specifications. Zbl 1087.68596Kugler, Hillel; Harel, David; Pnueli, Amir; Lu, Yuan; Bontemps, Yves 7 2005 Synthesis revisited: Generating statechart models from scenario-based requirements. Zbl 1075.68614Harel, David; Kugler, Hillel; Pnueli, Amir 7 2005 Shape analysis by predicate abstraction. Zbl 1111.68396Balaban, Ittai; Pnueli, Amir; Zuck, Lenore D. 5 2005 A discrete-time UML semantics for concurrency and communication in safety-critical applications. Zbl 1075.68048Damm, Werner; Josko, Bernhard; Pnueli, Amir; Votintseva, Angelika 3 2005 Bridging the gap between fair simulation and trace inclusion. Zbl 1082.68055Kesten, Yonit; Piterman, Nir; Pnueli, Amir 3 2005 IIV: An invisible invariant verifier. Zbl 1081.68603Balaban, Ittai; Fang, Yi; Pnueli, Amir; Zuck, Lenore D. 2 2005 Refining the undecidability frontier of hybrid automata. Zbl 1172.68521Mysore, Venkatesh; Pnueli, Amir 2 2005 Separating fairness and well-foundedness for the analysis of fair discrete systems. Zbl 1087.68066Pnueli, Amir; Podelski, Andreas; Rybalchenko, Andrey 1 2005 Translation and run-time validation of loop transformations. Zbl 1083.68555Zuck, Lenore; Pnueli, Amir; Goldberg, Benjamin; Barrett, Clark; Fang, Yi; Hu, Ying 1 2005 Model checking and abstraction to the aid of parameterized systems (a survey). Zbl 1072.68069Zuck, Lenore; Pnueli, Amir 10 2004 Liveness with invisible ranking. Zbl 1202.68248Fang, Yi; Piterman, Nir; Pnueli, Amir; Zuck, Lenore 3 2004 On recognizable timed languages. Zbl 1126.68459Maler, Oded; Pnueli, Amir 3 2004 Range allocation for separation logic. Zbl 1103.68079Talupur, Muralidhar; Sinha, Nishant; Strichman, Ofer; Pnueli, Amir 2 2004 Liveness with incomprehensible ranking. Zbl 1126.68474Fang, Yi; Piterman, Nir; Pnueli, Amir; Zuck, Lenore 2 2004 Formal modeling of C. elegans development: A scenario-based approach. Zbl 1053.92034Kam, Na’aman; Harel, David; Kugler, Hillel; Marelly, Rami; Pnueli, Amir; Hubbard, E. Jane Albert; Stern, Michael J. 6 2003 Parameterized verification by probabilistic abstraction. Zbl 1029.68104Arons, Tamarah; Pnueli, Amir; Zuck, Lenore 5 2003 tlpvs: A pvs-based ltl verification system. Zbl 1274.68202Pnueli, Amir; Arons, Tamarah 3 2003 Hybrid systems: computation and control. 6th international workshop, HSCC 2003, Prague, Czech Republic, April 3–5, 2003. Proceedings. Zbl 1017.00053 3 2003 Bridging the gap between fair simulation and trace inclusion. Zbl 1278.68178Kesten, Yonit; Piterman, Nir; Pnueli, Amir 2 2003 Model-checking and abstraction to the aid of parameterized systems. Zbl 1022.68580Pnueli, Amir; Zuck, Lenore 1 2003 Understanding UML: a formal semantics of concurrency and communication in real-time UML. Zbl 1254.68140Damm, Werner; Josko, Bernhard; Pnueli, Amir; Votintseva, Angelika 1 2003 Liveness with \({(0,1,\infty)}\)-counter abstraction. Zbl 1010.68095Pnueli, Amir; Xu, Jessie; Zuck, Lenore 17 2002 Complete proof system for QPTL. Zbl 1013.03012Kesten, Yonit; Pnueli, Amir 12 2002 A deductive proof system for CTL\(^{\ast}\). Zbl 1012.68119Pnueli, Amir; Kesten, Yonit 9 2002 Smart play-out of behavioral requirements. Zbl 1019.68622Harel, David; Kugler, Hillel; Marelly, Rami; Pnueli, Amir 9 2002 The small model property: How small can it be? Zbl 1012.03040Pnueli, Amir; Rodeh, Yoav; Strichman, Ofer; Siegel, Michael 7 2002 Network invariants in action. Zbl 1012.68131Kesten, Yonit; Pnueli, Amir; Shahar, Elad; Zuck, Lenore 4 2002 TimeC: A time constraint language for ILP processor compilation. Zbl 1019.68028Leung, Allen; Palem, Krishna V.; Pnueli, Amir 1 2002 Embedded systems: Challenges in specification and verification. Zbl 1027.68914Pnueli, Amir 1 2002 Automatic verification of probabilistic free choice. Zbl 1057.68644Zuck, Lenore; Pnueli, Amir; Kesten, Yonit 1 2002 Symbolic model checking with rich assertional languages. Zbl 0973.68119Kesten, Y.; Maler, O.; Marcus, M.; Pnueli, A.; Shahar, E. 33 2001 Automatic deductive verification with invisible invariants. Zbl 0978.68539Pnueli, Amir; Ruah, Sitvanit; Zuck, Lenore 19 2001 Parameterized verification with automatically computed inductive assertions. Zbl 0991.68541Arons, Tamarah; Pnueli, Amir; Ruah, Sitvanit; Xu, Ying; Zuck, Lenore 15 2001 From falsification to verification. Zbl 1052.68086Peled, Doron; Pnueli, Amir; Zuck, Lenore 8 2001 Beyond regular model checking. Zbl 1052.68084Fisman, Dana; Pnueli, Amir 5 2001 Range allocation for equivalence logic. Zbl 1052.68088Pnueli, Amir; Rodeh, Yoav; Shtrichman, Ofer 3 2001 Verification by augmented abstraction: The automata-theoretic view. Zbl 0983.68109Kesten, Yonit; Pnueli, Amir; Vardi, Moshe Y. 2 2001 Propositional temporal logics: Decidability and completeness. Zbl 1033.03009Lichtenstein, Orna; Pnueli, Amir 28 2000 Verification by augmented finitary abstraction. Zbl 1003.68069Kesten, Yonit; Pnueli, Amir 18 2000 Liveness and acceleration in parameterized verification. Zbl 0974.68521Pnueli, Amir; Shahar, Elad 12 2000 Control and data abstraction: The cornerstones of practical formal verification. Zbl 1059.68589Kesten, Yonit; Pnueli, Amir 11 2000 Verification of clocked and hybrid systems. Zbl 0957.68073Kesten, Yonit; Manna, Zohar; Pnueli, Amir 2 2000 A comparison of two verification methods for speculative instruction execution. Zbl 0971.68576Arons, Tamarah; Pnueli, Amir 2 2000 Formal verification of the Ricart-Agrawala algorithm. Zbl 1044.68677Sedletsky, Ekaterina; Pnueli, Amir; Ben-Ari, Mordechai 2 2000 Decidable integration graphs. Zbl 1045.68566Kesten, Y.; Pnueli, A.; Sifakis, J.; Yovine, S. 14 1999 Deciding equality formulas by small domains instantiations. Zbl 1046.68605Pnueli, Amir; Rodeh, Yoav; Shtrichman, Ofer; Siegel, Michael 12 1999 Orthogonal polyhedra: Representation and computation. Zbl 0947.68154Bournez, Olivier; Maler, Oded; Pnueli, Amir 7 1999 Verifying liveness by augmented abstraction. Zbl 0944.68128Kesten, Yonit; Pnueli, Amir 1 1999 On discretization of delays in timed automata and digital circuits. Zbl 0933.94045Asarin, Eugene; Maler, Oded; Pnueli, Amir 19 1998 The code validation tool (CVT). Automatic verification of a compilation process. Zbl 1022.68733Pnueli, A.; Shtrichman, O.; Siegel, M. 9 1998 Herbrand automata for hardware verification. Zbl 0940.68051Damm, W.; Pnueli, A.; Ruah, S. 2 1998 On the synthesis of discrete controllers for timed systems. Zbl 1379.68227Maler, Oded; Pnueli, Amir; Sifakis, Joseph 70 1995 Reachability analysis of dynamical systems having piecewise-constant derivatives. Zbl 0884.68050Asarin, Eugene; Maler, Oded; Pnueli, Amir 53 1995 Verification of parameterized programs. Zbl 0844.68079Manna, Zohar; Pnueli, Amir 26 1995 On the learnability of infinitary regular sets. Zbl 0834.68099Maler, Oded; Pnueli, Amir 19 1995 Special issue on Hybrid systems. Zbl 0879.00023 6 1995 Temporal proof methodologies for timed transition systems. Zbl 0820.68085Henzinger, Thomas A.; Manna, Zohar; Pnueli, Amir 15 1994 Proving partial order properties. Zbl 0803.68070Peled, Doron; Pnueli, Amir 10 1994 Temporal verification diagrams. Zbl 0942.03527Manna, Zohar; Pnueli, Amir 7 1994 Models for reactivity. Zbl 0790.68041Manna, Zohar; Pnueli, Amir 15 1993 Probabilistic verification. Zbl 0797.68112Pnueli, Amir; Zuck, Lenore D. 12 1993 System specification and refinement in temporal logic. Zbl 0919.03027Pnueli, Amir 4 1992 Characterization of temporal property classes. Zbl 1425.68252Chang, Edward; Manna, Zohar; Pnueli, Amir 3 1992 What good are digital clocks? Zbl 1425.68255Henzinger, Thomas A.; Manna, Zohar; Pnueli, Amir 3 1992 The temporal logic of reactive and concurrent systems. Specification. Zbl 0753.68003Manna, Zohar; Pnueli, Amir 194 1991 Completing the temporal picture. Zbl 0795.68133Manna, Zohar; Pnueli, Amir 26 1991 On the faithfulness of formal models. Zbl 0776.68041Manna, Zohar; Pnueli, Amir 2 1991 What is in a step: on the semantics of statecharts. Zbl 1493.68121Pnueli, A.; Shalev, M. 1 1991 Proving partial order liveness properties. Zbl 0765.68137Peled, Doron; Pnueli, Amir 6 1990 On the synthesis of an asynchronous reactive module. Zbl 0686.68015Pnueli, Amir; Rosner, Roni 172 1989 The anchored version of the temporal framework. (Tutorial). Zbl 0683.68031Manna, Z.; Pnueli, A. 25 1989 Completing the temporal picture. Zbl 0703.68075Manna, Zohar; Pnueli, Amir 7 1989 Temporal logic in specification. Altrincham, UK, April 8-10, 1987. Proceedings. Zbl 0718.68002 1 1989 Applications of temporal logic to the specification of real time systems. Zbl 0688.68024Pnueli, Amir; Harel, Eyal 5 1988 ...and 48 more Documents all cited Publications top 5 cited Publications all top 5 Cited by 2,272 Authors 32 Kupferman, Orna 29 Pnueli, Amir 26 Vardi, Moshe Ya’akov 23 Henzinger, Thomas A. 19 Chatterjee, Krishnendu 19 Larsen, Kim Guldstrand 15 Murano, Aniello 15 Peled, Doron A. 13 Baier, Christel 13 Esparza, Javier 13 Harel, David 13 Raskin, Jean-François 12 Best, Eike 12 Duan, Zhenhua 12 Majumdar, Rupak 12 Manna, Zohar 11 Alur, Rajeev 11 Bouyer, Patricia 11 Fisman, Dana 11 Kröning, Daniel 11 Legay, Axel 10 Abdulla, Parosh Aziz 10 Bournez, Olivier 10 de Alfaro, Luca 10 Maler, Oded 10 Mogavero, Fabio 10 Piterman, Nir 9 Asarin, Eugene 9 Bloem, Roderick 9 Grumberg, Orna 9 Katz, Shmuel 8 Bouajjani, Ahmed 8 Cimatti, Alessandro 8 Devillers, Raymond 8 Dixon, Clare 8 Halpern, Joseph Yehuda 8 Hesselink, Wim H. 8 Kwiatkowska, Marta Z. 8 Markey, Nicolas 8 Meseguer Guaita, José 8 Montanari, Angelo 8 Reynolds, Mark Alexander 8 Strichman, Ofer 8 Thiagarajan, Pazhamaneri Subramaniam 8 Zuck, Lenore D. 7 Avni, Guy 7 Basin, David A. 7 Brihaye, Thomas 7 Chebotarev, Anatoli N. 7 Clarke, Edmund Melson jun. 7 Doyen, Laurent 7 Faella, Marco 7 Finkbeiner, Bernd 7 Francez, Nissim 7 Gavril, Fanica 7 Jobstmann, Barbara 7 Jonsson, Bengt 7 Lange, Martin 7 Olderog, Ernst-Rüdiger 7 Rabinovich, Alexander 7 Tian, Cong 7 Zhang, Nan 7 Zimmermann, Martín G. 6 Bérard, Béatrice 6 David, Alexandre 6 Fernández Duque, David 6 Kesten, Yonit 6 Lime, Didier 6 Perelli, Giuseppe 6 Sankaranarayanan, Sriram 6 Schewe, Sven 6 Stewart, Lorna K. 6 Tonetta, Stefano 6 Viswanathan, Mahesh 6 Wąsowski, Andrzej 5 Angluin, Dana 5 Barrett, Clark W. 5 Bonakdarpour, Borzoo 5 Fahrenberg, Uli 5 Filiot, Emmanuel 5 Friedman, Emily P. 5 Girard, Antoine 5 Golumbic, Martin Charles 5 Haddad, Serge 5 Katoen, Joost-Pieter 5 Kulkarni, Sandeep S. 5 McIver, Annabelle K. 5 McMillan, Kenneth L. 5 Mondal, Sukumar 5 Moszkowski, Ben C. 5 Namjoshi, Kedar S. 5 Rezine, Ahmed 5 Rotem, Doron 5 Roux, Olivier H. 5 Roveri, Marco 5 Rybakov, Vladimir Vladimirovich 5 Schneider, Gerardo 5 Sharygina, Natasha 5 Sifakis, Joseph 5 Silva, Alexandra ...and 2,172 more Authors all top 5 Cited in 149 Serials 217 Theoretical Computer Science 89 Information and Computation 89 Formal Methods in System Design 78 Formal Aspects of Computing 63 Acta Informatica 52 Journal of Computer and System Sciences 47 Information Processing Letters 36 Distributed Computing 24 Discrete Applied Mathematics 24 Journal of Automated Reasoning 24 Discrete Event Dynamic Systems 19 Annals of Mathematics and Artificial Intelligence 17 Automatica 16 The Journal of Logic and Algebraic Programming 15 Discrete Mathematics 15 Science of Computer Programming 15 Logical Methods in Computer Science 12 Journal of Computer Science and Technology 12 International Journal of Foundations of Computer Science 11 Artificial Intelligence 11 ACM Transactions on Computational Logic 9 Cybernetics and Systems Analysis 9 Journal of Applied Non-Classical Logics 9 Journal of Logical and Algebraic Methods in Programming 8 Journal of Applied Logic 8 Nonlinear Analysis. Hybrid Systems 7 Annals of Pure and Applied Logic 7 Journal of Symbolic Computation 7 European Journal of Control 6 Computing 6 Mathematical Systems Theory 6 Networks 6 International Journal of Computer Mathematics 5 Information Sciences 5 The Journal of Symbolic Logic 5 Programming and Computer Software 5 MSCS. Mathematical Structures in Computer Science 5 Journal of Logic, Language and Information 5 Fundamenta Informaticae 4 International Journal of Control 4 Journal of Combinatorial Theory. Series B 4 Order 4 International Journal of Parallel Programming 4 Journal of the ACM 3 Applied Mathematics and Computation 3 Journal of Soviet Mathematics 3 RAIRO, Informatique Théorique 3 Studia Logica 3 Synthese 3 Cybernetics 3 Systems & Control Letters 3 Algorithmica 3 Real-Time Systems 3 RAIRO. Informatique Théorique et Applications 3 Theory of Computing Systems 3 Higher-Order and Symbolic Computation 3 Theory and Practice of Logic Programming 3 Sādhanā 3 Computer Science Review 2 Computers & Mathematics with Applications 2 International Journal of General Systems 2 International Journal of Systems Science 2 Journal of the Franklin Institute 2 BIT 2 Journal of Graph Theory 2 Journal of Mathematical Psychology 2 Mathematics and Computers in Simulation 2 Notre Dame Journal of Formal Logic 2 International Journal of Production Research 2 Graphs and Combinatorics 2 Applied Stochastic Models and Data Analysis 2 Journal of Complexity 2 New Generation Computing 2 SIAM Journal on Discrete Mathematics 2 Machine Learning 2 JETAI. Journal of Experimental & Theoretical Artificial Intelligence 2 International Journal of Robust and Nonlinear Control 2 The Journal of Artificial Intelligence Research (JAIR) 2 Parallel Algorithms and Applications 2 Journal of Combinatorial Optimization 2 Journal of Applied Mathematics and Computing 2 BIT. Nordisk Tidskrift for Informationsbehandling 2 Mathematics in Computer Science 2 Science China. Information Sciences 2 Frontiers of Computer Science in China 2 Frontiers of Computer Science 2 Modelirovanie i Analiz Informatsionnykh Sistem 1 International Journal of Theoretical Physics 1 Algebra and Logic 1 Calcolo 1 International Journal of Computer & Information Sciences 1 Journal of Computational and Applied Mathematics 1 Journal of Philosophical Logic 1 Mathematische Nachrichten 1 Nonlinear Analysis. Theory, Methods & Applications. Series A: Theory and Methods 1 Proceedings of the American Mathematical Society 1 Siberian Mathematical Journal 1 Moscow University Computational Mathematics and Cybernetics 1 Advances in Applied Mathematics 1 Mathematical Social Sciences ...and 49 more Serials all top 5 Cited in 34 Fields 1,324 Computer science (68-XX) 439 Mathematical logic and foundations (03-XX) 122 Systems theory; control (93-XX) 115 Combinatorics (05-XX) 90 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 48 Operations research, mathematical programming (90-XX) 25 Information and communication theory, circuits (94-XX) 24 Order, lattices, ordered algebraic structures (06-XX) 17 Biology and other natural sciences (92-XX) 10 Dynamical systems and ergodic theory (37-XX) 9 Numerical analysis (65-XX) 8 Probability theory and stochastic processes (60-XX) 7 Ordinary differential equations (34-XX) 5 General and overarching topics; collections (00-XX) 5 Calculus of variations and optimal control; optimization (49-XX) 4 Quantum theory (81-XX) 3 History and biography (01-XX) 3 Category theory; homological algebra (18-XX) 3 Statistics (62-XX) 2 Field theory and polynomials (12-XX) 2 Commutative algebra (13-XX) 2 Group theory and generalizations (20-XX) 2 Measure and integration (28-XX) 2 Convex and discrete geometry (52-XX) 2 General topology (54-XX) 2 Mechanics of particles and systems (70-XX) 1 General algebraic systems (08-XX) 1 Number theory (11-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Partial differential equations (35-XX) 1 Difference and functional equations (39-XX) 1 Operator theory (47-XX) 1 Fluid mechanics (76-XX) 1 Mathematics education (97-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.