| Year |
Citation |
Score |
| 2019 |
Ferrère T, Maler O, Ničković D, Pnueli A. From Real-time Logic to Timed Automata Journal of the Acm. 66: 1-31. DOI: 10.1145/3286976 |
0.357 |
|
| 2012 |
Kupferman O, Pnueli A, Vardi MY. Once and for all Journal of Computer and System Sciences. 78: 981-996. DOI: 10.1016/J.Jcss.2011.08.006 |
0.384 |
|
| 2012 |
Balaban I, Pnueli A, Sa'Ar Y, Zuck LD. Verification of multi-linked heaps Journal of Computer and System Sciences. 78: 853-876. DOI: 10.1016/J.Jcss.2011.08.003 |
0.379 |
|
| 2012 |
Asarin E, Mysore VP, Pnueli A, Schneider G. Low dimensional hybrid systems - Decidable, undecidable, dont know Information and Computation. 211: 138-159. DOI: 10.1016/J.Ic.2011.11.006 |
0.321 |
|
| 2010 |
Balaban I, Pnueli A, Zuck LD. Proving the refuted: Symbolic model checkers as proof generators Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 5930: 221-236. DOI: 10.1007/978-3-642-11512-7_14 |
0.333 |
|
| 2009 |
Pnueli A, Klein U. Synthesis of programs from temporal property specifications 2009 7th Ieee-Acm International Conference On Formal Methods and Models For Co-Design, Memocode '09. 1-7. DOI: 10.1109/MEMCOD.2009.5185372 |
0.321 |
|
| 2009 |
Kugler H, Plock C, Pnueli A. Controller synthesis from LSC requirements Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 5503: 79-93. DOI: 10.1007/978-3-642-00593-0_6 |
0.605 |
|
| 2008 |
Kam N, Kugler H, Marelly R, Appleby L, Fisher J, Pnueli A, Harel D, Stern MJ, Hubbard EJ. A scenario-based approach to modeling development: a prototype model of C. elegans vulval fate specification. Developmental Biology. 323: 1-5. PMID 18706404 DOI: 10.1016/J.Ydbio.2008.07.030 |
0.625 |
|
| 2008 |
Gabbay DM, Pnueli A. A sound and complete deductive system for CTL* verification* Logic Journal of the Igpl. 16: 499-536. DOI: 10.1093/Jigpal/Jzn018 |
0.419 |
|
| 2007 |
Kugler H, Plock C, Pnueli A. Synthesizing reactive systems from LSC requirements using the play-engine Proceedings of the Conference On Object-Oriented Programming Systems, Languages, and Applications, Oopsla. 801-802. DOI: 10.1145/1297846.1297895 |
0.605 |
|
| 2007 |
Balaban I, Pnueli A, Zuck LD. Modular ranking abstraction International Journal of Foundations of Computer Science. 18: 5-44. DOI: 10.1142/S0129054107004553 |
0.403 |
|
| 2007 |
Bloem R, Galler S, Jobstmann B, Piterman N, Pnueli A, Weiglhofer M. Specify, Compile, Run: Hardware from PSL Electronic Notes in Theoretical Computer Science. 190: 3-16. DOI: 10.1016/J.Entcs.2007.09.004 |
0.398 |
|
| 2007 |
Kugler H, Pnueli A, Stern MJ, Hubbard EJA. "Don't care" modeling: A logical framework for developing predictive system models Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 4424: 343-357. |
0.511 |
|
| 2006 |
Piterman N, Pnueli A, Sa'ar Y. Synthesis of reactive(1) designs Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 3855: 364-380. DOI: 10.1016/J.Jcss.2011.08.007 |
0.372 |
|
| 2006 |
Pnueli A, Zaks A, Zuck L. Monitoring Interfaces for Faults Electronic Notes in Theoretical Computer Science. 144: 73-89. DOI: 10.1016/J.Entcs.2006.02.005 |
0.334 |
|
| 2006 |
Pnueli A, Strichman O. Reduced functional consistency of uninterpreted functions Electronic Notes in Theoretical Computer Science. 144: 53-65. DOI: 10.1016/J.Entcs.2005.12.006 |
0.324 |
|
| 2006 |
Kesten Y, Pnueli A, Raviv LO, Shahar E. Model checking with strong fairness Formal Methods in System Design. 28: 57-84. DOI: 10.1007/s10703-006-4342-y |
0.332 |
|
| 2006 |
Fang Y, Piterman N, Pnueli A, Zuck L. Liveness with invisible ranking International Journal On Software Tools For Technology Transfer. 8: 261-279. DOI: 10.1007/S10009-005-0193-X |
0.426 |
|
| 2006 |
Pnueli A, Zaks A. PSL model checking and run-time verification via testers Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 4085: 573-586. |
0.303 |
|
| 2005 |
Damm W, Josko B, Pnueli A, Votintseva A. A discrete-time UML semantics for concurrency and communication in safety-critical applications Science of Computer Programming. 55: 81-115. DOI: 10.1016/J.Scico.2004.05.012 |
0.406 |
|
| 2005 |
Hu Y, Barrett C, Goldberg B, Pnueli A. Validating more loop optimizations Electronic Notes in Theoretical Computer Science. 141: 69-84. DOI: 10.1016/J.Entcs.2005.02.044 |
0.329 |
|
| 2005 |
Harel D, Kugler H, Pnueli A. Synthesis revisited: Generating statechart models from scenario-based requirements Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 3393: 309-324. |
0.631 |
|
| 2005 |
Balaban I, Pnueli A, Zuck LD. Shape analysis by predicate abstraction Lecture Notes in Computer Science. 3385: 164-180. |
0.315 |
|
| 2005 |
Kugler H, Harel D, Pnueli A, Lu Y, Bontemps Y. Temporal logic for scenario-based specifications Lecture Notes in Computer Science. 3440: 445-460. |
0.605 |
|
| 2005 |
Pnueli A, Podelski A, Rybalchenko A. Separating fairness and well-foundedness for the analysis of fair discrete systems Lecture Notes in Computer Science. 3440: 124-139. |
0.326 |
|
| 2004 |
Harel D, Kugler H, Pnueli A. Smart play-out extended: Time and forbidden elements Proceedings - Fourth International Conference On Quality Software, Qsic 2004. 2-11. DOI: 10.1109/QSIC.2004.1357938 |
0.599 |
|
| 2004 |
Zuck L, Pnueli A. Model checking and abstraction to the aid of parameterized systems (a survey) Computer Languages, Systems and Structures. 30: 139-169. DOI: 10.1016/J.Cl.2004.02.006 |
0.429 |
|
| 2004 |
Pnueli A, Arons T. TLPVS: A PVS-based LTL verification system Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2772: 598-625. DOI: 10.1007/978-3-540-39910-0_26 |
0.449 |
|
| 2004 |
Arons T, Hooman J, Kugler H, Pnueli A, Van Der Zwaag MD. Deductive Verification of UML Models in TLPVS Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 3273: 335-349. DOI: 10.1007/978-3-540-30187-5_24 |
0.662 |
|
| 2003 |
Mishra B, Daruwala RS, Zhou Y, Ugel N, Policriti A, Antoniotti M, Paxia S, Rejali M, Rudra A, Cherepinsky V, Silver N, Casey W, Piazza C, Simeoni M, Barbano P, ... ... Pnueli A, et al. A sense of life: computational and experimental investigations with models of biochemical and evolutionary processes. Omics : a Journal of Integrative Biology. 7: 253-68. PMID 14583115 DOI: 10.1089/153623103322452387 |
0.358 |
|
| 2003 |
Harel D, Kugler H, Marelly R, Pnueli A. Smart play-out Proceedings of the Conference On Object-Oriented Programming Systems, Languages, and Applications, Oopsla. 68-69. DOI: 10.1145/949344.949353 |
0.462 |
|
| 2003 |
Kesten Y, Piterman N, Pnueli A. Bridging the gap between fair simulation and trace inclusion Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2725: 381-393. DOI: 10.1016/J.Ic.2005.01.006 |
0.378 |
|
| 2003 |
Langberg M, Pnueli A, Rodeh Y. The ROBDD size of simple CNF formulas Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2860: 363-377. DOI: 10.1007/978-3-540-39724-3_32 |
0.374 |
|
| 2003 |
Kam N, Harel D, Kugler H, Marelly R, Pnueli A, Albert Hubbard EJ, Stern MJ. Formal Modeling of C. elegans development: A Scenario-based approach Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2602: 4-20. DOI: 10.1007/3-540-36481-1_2 |
0.595 |
|
| 2003 |
Pnueli A, Zuck L. Model-checking and abstraction to the aid of parameterized systems Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2575: 4. |
0.324 |
|
| 2002 |
Kesten Y, Pnueli A. Complete proof system for QPTL Journal of Logic and Computation. 12: 701-745. DOI: 10.1093/Logcom/12.5.701 |
0.407 |
|
| 2002 |
Leung A, Palem KV, Pnueli A. TimeC: A time constraint language for ILP processor compilation Constraints. 7: 75-115. DOI: 10.1023/A:1015131814255 |
0.413 |
|
| 2002 |
Pnueli A, Rodeh Y, Strichman O, Siegel M. The small model property: How small can it be? Information and Computation. 178: 279-293. DOI: 10.1016/S0890-5401(02)93175-5 |
0.352 |
|
| 2002 |
Harel D, Kugler H, Marelly R, Pnueli A. Smart play-out of behavioral requirements Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2517: 378-398. |
0.596 |
|
| 2001 |
Kesten Y, Maler O, Marcus M, Pnueli A, Shahar E. Symbolic model checking with rich assertional languages Theoretical Computer Science. 256: 93-112. DOI: 10.1016/S0304-3975(00)00103-1 |
0.444 |
|
| 2001 |
Arons T, Pnueli A, Ruah S, Xu Y, Zuck L. Parameterized verification with automatically computed inductive assertions Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2102: 221-234. DOI: 10.1007/3-540-44585-4_19 |
0.335 |
|
| 2001 |
Kesten Y, Pnueli A, Vardi MY. Verification by augmented abstraction: The automata-theoretic view Journal of Computer and System Sciences. 62: 668-690. DOI: 10.1006/Jcss.2000.1744 |
0.412 |
|
| 2001 |
Fisman D, Pnueli A. Beyond regular model checking (extended abstract) Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2245: 156-170. |
0.328 |
|
| 2001 |
Peled D, Pnueli A, Zuck L. From falsification to verification Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2245: 292-304. |
0.32 |
|
| 2000 |
Kesten Y, Pnueli A. Control and data abstraction: The cornerstones of practical formal verification International Journal On Software Tools For Technology Transfer. 2: 328-342. DOI: 10.1007/S100090050040 |
0.452 |
|
| 2000 |
Kesten Y, Manna Z, Pnueli A. Verification of clocked and hybrid systems Acta Informatica. 36: 837-912. DOI: 10.1007/S002360050177 |
0.434 |
|
| 2000 |
Kesten Y, Pnueli A. Verification by augmented finitary abstraction Information and Computation. 163: 203-243. DOI: 10.1006/Inco.2000.3000 |
0.408 |
|
| 2000 |
Pnueli A, Shahar E. Liveness and acceleration in parameterized verification Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1855: 328-343. |
0.373 |
|
| 1999 |
Jonsson B, Pnueli A, Rump C. Proving refinement using transduction Distributed Computing. 12: 129-149. DOI: 10.1007/S004460050062 |
0.386 |
|
| 1999 |
Kesten Y, Pnueli A, Sifakis J, Yovine S. Decidable Integration Graphs Information and Computation. 150: 209-243. DOI: 10.1006/Inco.1998.2774 |
0.341 |
|
| 1999 |
Kesten Y, Pnueli A. Verifying liveness by augmented abstraction Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1683: 141-156. |
0.314 |
|
| 1998 |
Asarin E, Maler O, Pnueli A, Sifakis J. Controller Synthesis for Timed Automata 1 Ifac Proceedings Volumes. 31: 447-452. DOI: 10.1016/S1474-6670(17)42032-5 |
0.349 |
|
| 1998 |
Pnueli A, Shankar N, Singerman E. Fair synchronous transition systems and their liveness proofs Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1486: 198-209. DOI: 10.1007/Bfb0055348 |
0.427 |
|
| 1998 |
Kesten Y, Pnueli A. Modularization and abstraction: The keys to practical formal verification Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1450: 54-71. |
0.358 |
|
| 1998 |
Kesten Y, Pnueli A, Raviv LO. Algorithmic verification of linear temporal logic specifications Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1443: 1-16. |
0.323 |
|
| 1998 |
Pnueli A. —Invited talk— deductive vs. model-theoretic approaches to formal verification Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1421: 301. |
0.329 |
|
| 1996 |
Kesten Y, Manna Z, Pnueli A. Verifying clocked transition systems Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1066: 13-40. DOI: 10.1007/BFb0020933 |
0.333 |
|
| 1996 |
Pnueli A, Shahar E. A platform for combining deductive with algorithmic verification Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1102: 184-195. DOI: 10.1007/3-540-61474-5_68 |
0.376 |
|
| 1995 |
Asarin E, Maler O, Pnueli A. Reachability analysis of dynamical systems having piecewise-constant derivatives Theoretical Computer Science. 138: 35-65. DOI: 10.1016/0304-3975(94)00228-B |
0.331 |
|
| 1995 |
Maler O, Pnueli A. On the Learnability of Infinitary Regular Sets Information and Computation. 118: 316-326. DOI: 10.1006/Inco.1995.1070 |
0.332 |
|
| 1994 |
Peled D, Pnueli A. Proving partial order properties Theoretical Computer Science. 126: 143-182. DOI: 10.1016/0304-3975(94)90009-4 |
0.377 |
|
| 1994 |
Henzinger TA, Manna Z, Pnueli A. Temporal Proof Methodologies for Timed Transition-Systems Information and Computation. 112: 273-337. DOI: 10.1006/Inco.1994.1060 |
0.426 |
|
| 1993 |
Manna Z, Pnueli A. Models for reactivity Acta Informatica. 30: 609-678. DOI: 10.1007/Bf01191722 |
0.479 |
|
| 1993 |
Pnueli A, Zuck LD. Probabilistic Verification Information and Computation. 103: 1-29. DOI: 10.1006/Inco.1993.1012 |
0.362 |
|
| 1988 |
Harel D, Lachover H, Naamad A, Pnueli A, Politi M, Sherman R, Shtul-Trauring A. STATEMATE: a working environment for the development of complex reactive systems . 1-3. DOI: 10.1109/32.54292 |
0.413 |
|
| 1988 |
Dori D, Pnueli A. The grammar of dimensions in machine drawings Computer Vision, Graphics, and Image Processing. 42: 1-18. DOI: 10.1016/0734-189X(88)90139-9 |
0.333 |
|
| 1987 |
Shi Y, Prywes N, Szymanski B, Pnueli A. Very High Level Concurrent Programming Ieee Transactions On Software Engineering. 1038-1046. DOI: 10.1109/Tse.1987.233791 |
0.453 |
|
| 1986 |
Pnueli A, Zuck L. Verification of multiprocess probabilistic protocols Distributed Computing. 1: 53-72. DOI: 10.1007/Bf01843570 |
0.383 |
|
| 1984 |
Sherman R, Pnueli A, Harel D. IS THE INTERESTING PART OF PROCESS LOGIC UNINTERESTING? : A TRANSLATION FROM PL TO PDL Siam Journal On Computing. 13: 825-839. DOI: 10.1137/0213051 |
0.344 |
|
| 1984 |
Sharir M, Pnueli A, Hart S. Verification of Probabilistic Programs Siam Journal On Computing. 13: 292-314. DOI: 10.1137/0213021 |
0.353 |
|
| 1984 |
Apt KR, Pnueli A, Stavi J. Fair termination revisited-with delay Theoretical Computer Science. 33: 65-84. DOI: 10.1016/0304-3975(84)90103-8 |
0.327 |
|
| 1984 |
Francez N, Lehmann D, Pnueli A. A linear-history semantics for languages for distributed programming Theoretical Computer Science. 32: 25-46. DOI: 10.1016/0304-3975(84)90022-7 |
0.365 |
|
| 1984 |
Manna Z, Pnueli A. Adequate proof principles for invariance and liveness properties of concurrent programs Science of Computer Programming. 4: 257-289. DOI: 10.1016/0167-6423(84)90003-0 |
0.376 |
|
| 1983 |
Hart S, Sharir M, Pnueli A. Termination of Probabilistic Concurrent Program Acm Transactions On Programming Languages and Systems (Toplas). 5: 356-380. DOI: 10.1145/2166.357214 |
0.364 |
|
| 1983 |
Harel D, Pnueli A, Stavi J. Propositional dynamic logic of nonregular programs Journal of Computer and System Sciences. 26: 222-243. DOI: 10.1016/0022-0000(83)90014-4 |
0.338 |
|
| 1983 |
Ben-Ari M, Pnueli A, Manna Z. The temporal logic of branching time Acta Informatica. 20: 207-226. DOI: 10.1007/Bf01257083 |
0.406 |
|
| 1982 |
Ben-Ari M, Halpern JY, Pnueli A. Deterministic propositional dynamic logic: Finite models, complexity, and completeness Journal of Computer and System Sciences. 25: 402-417. DOI: 10.1016/0022-0000(82)90018-6 |
0.328 |
|
| 1981 |
Pnueli A, Slutzki G. Automatic Programming of Finite State Linear Programs Siam Journal On Computing. 10: 519-535. DOI: 10.1137/0210038 |
0.356 |
|
| 1981 |
Pnueli A. The temporal semantics of concurrent programs Theoretical Computer Science. 13: 45-60. DOI: 10.1016/0304-3975(81)90110-9 |
0.38 |
|
| 1978 |
Francez N, Pnueli A. A proof method for cyclic programs Acta Informatica. 9: 133-157. DOI: 10.1007/Bf00289074 |
0.386 |
|
| 1977 |
Francez N, Klebansky B, Pnueli A. Backtracking in recursive computations Acta Informatica. 8: 125-144. DOI: 10.1007/Bf00289245 |
0.383 |
|
| 1974 |
Manna Z, Pnueli A. Axiomatic approach to total correctness of programs Acta Informatica. 3: 243-263. DOI: 10.1007/Bf00288637 |
0.334 |
|
| 1973 |
Ashcroft E, Manna Z, Pnueli A. Decidable Properties of Monadic Functional Schemas Journal of the Acm (Jacm). 20: 489-499. DOI: 10.1145/321765.321780 |
0.325 |
|
| 1971 |
Commoner F, Holt AW, Even S, Pnueli A. Marked directed graphs Journal of Computer and System Sciences. 5: 511-523. DOI: 10.1016/S0022-0000(71)80013-2 |
0.35 |
|
| 1970 |
Manna Z, Pnueli A. Formalization of Properties of Functional Programs Journal of the Acm (Jacm). 17: 555-569. DOI: 10.1145/321592.321606 |
0.331 |
|
| 1968 |
Pnueli A, Pekeris CL. Free Tidal Oscillations in Rotating Flat Basins of the Form of Rectangles and of Sectors of Circles Philosophical Transactions of the Royal Society A. 263: 149-171. DOI: 10.1098/Rsta.1968.0009 |
0.533 |
|
| Show low-probability matches. |