Publications

Follow paper's title for abstract

Link's may lead to sites with restricted access

1998

1999

I. Gordin, R. Leviathan, and A. Pnueli. Validating the translation of an industrial optimizing compiler. In Proc. 2nd International Symposium on Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, Taiwan, November 2004. © Springer-Verlag. (Gzipped PostScript, 17 pages, 115658 bytes) (PDF, 206353 bytes)
Y. Kesten and A. Pnueli. A compositional approach to CTL^* verification. © Theoretical Computer Science, 2004. to appear. (Gzipped PostScript, 35 pages, 151181 bytes) (PDF, 382954 bytes)
D. Harel and H. Kugler. The rhapsody semantics of statecharts (or, on the executable core of UML), 2004. to appear.
S. Efroni, D. Harel, and I.R. Cohen. Multidisciplinary Approaches to Theory in Medicine, chapter Modeling and Simulation of the Thymus. Elsevier, 2004. to appear.
D. Barak, D. Harel, and R. Marelly. Interplay: Horizontal scale-up and transition to design in scienario-based programming. In J. Desel, W. Reisig, and G. Rozenberg, editors, Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science. © Springer-Verlag, 2004. (PDF, 489157 bytes)
T. Arons. Verification of an advanced mips-type out-of-order execution algorithm. In Proc. 16th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, pages 414-426, Boston, MA, USA, July 2004. © Springer-Verlag. (Gzipped PostScript, 13 pages, 96016 bytes) (PDF, 243798 bytes)
N. Piterman and Vardi M.Y. Global model-checking for infinite-state systems. In 16th. International Conference on Computer Aided Verification, Lecture Notes in Computer Science, pages 387-400, Boston, MA, USA, July 2004. © Springer-Verlag. (Gzipped PostScript, 21 pages, 106067 bytes) (PDF, 247696 bytes)
J. Fisher, D. Harel, E.J.A. Hubbard, N. Piterman, M.J. Stern, and N. Swerdlin. Combining state-based and scenario-based approaches in modeling biological systems. In 2nd International Workshop on Computational Methods in Systems Biology, Lecture Notes in Computer Science, Paris, France, May 2004. © Springer-Verlag.
M. Kyas, H. Fecher, F.S. de Boer, J. Jacob, J. Hooman, M. van der Zwaag, T. Arons, , and H. Kugler. Formalizing UML models and OCL constraints in PVS. In Proc. International Workshop on Semantic Foundation of Engineering Design Languages, Barcelona, Spain, March 2004. (PDF, 330091 bytes)
O. Maler and A. Pnueli. On recognizable timed languages. In 7th International Conference on Foundations of Software Science and Computation Structures, volume 2987 of Lecture Notes in Computer Science, pages 348-362, Barcelona, Spain, March 2004. © Springer-Verlag. (Springer PDF)
Y. Fang, N. Piterman, A. Pnueli, and L. Zuck. Liveness with incomprehensible ranking. In 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of Lecture Notes in Computer Science, pages 482-496, Bercelona, Spain, March 2004. © Springer-Verlag. (Gzipped PostScript, 15 pages, 121960 bytes) (PDF, 151544 bytes)
Y. Fang, N. Piterman, A. Pnueli, and L. Zuck. Liveness with invisible ranking. In 5th International Conference on Verification, Model Checking and Abstract Interpretation, volume 2937 of Lecture Notes in Computer Science, pages 223-238, Venice, Italy, January 2004. © Springer-Verlag. (Gzipped PostScript, 13 pages, 58233 bytes) (PDF, 154583 bytes)
T. Arons and A. Pnueli. TLPVS : A PVS-based LTL verification system. In N. Dershowitz, editor, Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday, volume 2772 of Lecture Notes in Computer Science, pages 598-625. © Springer-Verlag, 2004. (Gzipped PostScript, 28 pages, 136253 bytes) (PDF, 375289 bytes)
O. Kupferman, N. Piterman, and M. Y. Vardi. Fair equivalence relations. In N. Dershowitz, editor, Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, volume 2772 of Lecture Notes in Computer Science, pages 702-732. © Springer-Verlag, 2004. (Gzipped PostScript, 31 pages, 3101562 bytes) (PDF, 1357359 bytes)
L. Carmel, D. Harel, and Y. Koren. Combining hierarchy and energy drawing directed graphs. IEEE transactions on Visualizations and Computer Graphics, 10(1):46-57, January-February 2004. (IEEE PDF)

2003

D. Harel, S. Efroni, and I.R. Cohen. Reactive animation. In Proc. 1st International Symposium on Formal Methods for Components and Objects, volume 2852 of Lecture Notes in Computer Science, pages 136-153, Leiden, The Netherlands, November 2003. © Springer-Verlag. (PDF, 214444 bytes)
D. Harel and R. Marelly. Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. © Springer-Verlag, 2003.
M. Langberg, A. Pnueli, and Y. Rodeh. The robdd size of simple cnf formulas. In proceedings 12^th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science, L'Aquila, Italy, October 2003. © Springer-Verlag. (Gzipped PostScript, 15 pages, 112182 bytes) (PDF, 263285 bytes)
Y. Koren. On spectral graph drawing. In Procceedings 9^th International Computing and Combinatorics Conference, Lecture Notes in Computer Science, Big Sky, MT, USA, July 2003. © Springer-Verlag. (PDF, 660428 bytes)
C. Eisner, D. Fisman, J. Havlicek, Y. Lustig, A. McIsaac, and D. Van Campenhout. Reasoning with temporal logic on truncated paths. In Proceedings of 15^th International Conference on Computer Aided Verification, volume 2775 of Lecture Notes in Computer Science, pages 27-39, Boulder, CO, USA, July 2003. © Springer-Verlag. (PDF, 195325 bytes)
Y. Kesten, N. Piterman, and A. Pnueli. Bridging the gap between fair simulation and trace inclusion. In Proceedings of 15^th International Conference on Computer Aided Verification, volume 2775 of Lecture Notes in Computer Science, pages 381-393, Boulder, CO, USA, July 2003. © Springer-Verlag. (Gzipped PostScript, 21 pages, 97297 bytes) (PDF, 281026 bytes)
C. Eisner, D. Fisman, J. Havlicek, A. McIsaac, and D. Van Campenhout. The definition of a temporal clock operator. In Proceedings of 30^th International Colloquium on Automata Languages and Programming, volume 2719 of Lecture Notes in Computer Science, pages 857-870, Eindhoven, The Netherlands, June 2003. © Springer-Verlag. (PDF, 193998 bytes)
N. Piterman and M.Y. Vardi. Micro macro stack systems -- a new frontier of elementary decidability for sequential systems. In Proc. 18th IEEE Symposium on Logic in Computer Science, pages 381-390, Ottawa, Canada, June 2003. © IEEE, IEEE society press. (Gzipped PostScript, 15 pages, 102769 bytes) (PDF, 305298 bytes)
T. Arons, A. Pnueli, and L. Zuck. Parameterized verification by probabilistic abstraction. In Proceedings 6^th International Conference on Foundations of Software Science and Computational Structures, volume 2620 of Lecture Notes in Computer Science, pages 87-102, Warsaw, Poland, April 2003. © Springer-Verlag. (Gzipped PostScript, 16 pages, 126112 bytes) (PDF, 230017 bytes)
N. Kam, D. Harel, H. Kugler, R. Marelly, A. Pnueli, J. Hubbard, and M. Stern. Formal modeling of c. elegans development: A scenario-based approach. In First International Workshop on Computational Methods in Systems Biology, volume 2602 of Lecture Notes in Computer Science, pages 4-20, Rovereto, Italy, February 2003. © Springer-Verlag. (PDF, 240844 bytes)
N. Piterman and M. Vardi. From bidirectionality to alternation. Theoretical Computer Science, 295(1-3):295-321, February 2003. (Gzipped PostScript, 24 pages, 140168 bytes) (PDF, 310701 bytes)
S. Efroni, D. Harel, and I.R. Cohen. Towards rigorous comprehension of biological complexity: Modeling, execution and visualization of thymic t-cell maturation. Genome Research, 2003. special issue on Systems Biology, In press.
D. Harel and P.S. Thiagarajan. Message sequence charts. In L. Lavagno, G. Martin, and B. Selic, editors, UML for Real: Design of Embedded Real-time Systems. Kluwer Academic Press, 2003.

2002

Y. Kesten and A. Pnueli. Complete proof system for QPTL. Journal of Logic and Computation, 12(5):701-745, December 2002. (Gzipped PostScript, 51 pages, 209633 bytes) (PDF, 561383 bytes)
R. Marelly, D. Harel, and H. Kugler. Multiple instances and symbolic variables in executable sequence charts. In 17th Annual Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 83-100, Seattle, Washington, USA, November 2002. ACM, © ACM. (PDF) (ACM PDF)
D. Harel, H. Kugler, R. Marelly, and A. Pnueli. Smart play-out of behavioral requirements. In 4th International Conference on Formal Methods in Computer-Aided Design, volume 2517 of Lecture Notes in Computer Science, pages 378-398, Portland, Oregon, USA, November 2002. © Springer-Verlag. (Springer PDF)
D. Harel. A grand challenge for computing: Full reactive modeling of a multi-cellular animal. In Workshop on Grand Challenges for Computing Research, Edinburgh, Scotland, November 2002. The UK Computing Research Committee. Position Paper. (Gzipped PostScript, 43845 bytes)
A. Pnueli, Y. Rodeh, O. Strichman, and M. Siegel. The small model property: How small can it be? Information and Computation, 178(1):279-293, October 2002. (PostScript)
D. Harel. Can behavioral requirements be executed? (and why would we want to do so?). In Proceedings 2^nd International Workshop on Embedded Software, volume 2491 of Lecture Notes in Computer Science, pages 30-31, Grenoble, France, October 2002. © Springer-Verlag. (Gzipped PostScript, 2 pages, 49178 bytes)
D. Harel and R. Marelly. Playing with time: On the specification and execution of time-enriched lscs. In 10th IEEE International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, Fort Worth, Texas, USA, October 2002. IEEE, © IEEE computer society press. (PDF)
R. Leviathan and A. Pnueli. Validating software pipelining optimizations. In Proc. International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, volume 314, pages 280-287, Grenoble, France, October 2002. ACM, © ACM. (Gzipped PostScript, 8 pages, 147719 bytes) (PDF, 155039 bytes)
Y. Koren, L. Carmel, and D. Harel. Ace: A fast multiscale eigenvectors computation for drawing huge graphs. In Proc. IEEE Symposium on Information Visualization 2002, pages 137-144, Boston, MA, USA, October 2002. IEEE computer society press. (Gzipped PostScript, 8 pages, 831765 bytes) (PDF, 801977 bytes)
O. Kupferman, N. Piterman, and M. Vardi. Pushdown specifications. In 9th International Conference on Logic for Programming Artificial Intelligence and Reasoning, volume 2514 of Lecture Notes in Artificial Inteligence, pages 262-277, Tbilisi, Georgia, October 2002. © Springer-Verlag. (Gzipped PostScript, 19 pages, 79803 bytes) (PDF, 204883 bytes)
D. Harel, L. Carmel, and Y. Koren. Drawing directed graphs using one-dimensional optimization. In Proc. of 10th International Symposium on Graph Drawing, volume 2528 of Lecture Notes in Computer Science, pages 193-206, Irvine, CA, USA, August 2002. © Springer-Verlag. (Gzipped PostScript, 24 pages, 213819 bytes) (PDF, 294947 bytes)
D. Harel and Y. Koren. Graph drawing by high-dimensional embedding. In Proc. of 10th International Symposium on Graph Drawing, volume 2528 of Lecture Notes in Computer Science, pages 207-219, Irvine, CA, USA, August 2002. © Springer-Verlag. (Gzipped PostScript, 12 pages, 2068148 bytes) (PDF, 2330914 bytes)
Y. Kesten, A. Pnueli, E. Shahar, and L. Zuck. Network invariants in action. In Proc. 13th Conference on Concurrency Theory, volume 2421 of Lecture Notes in Computer Science, pages 101-115, Brno, Czech Republic, August 2002. © Springer-Verlag. (Gzipped PostScript, 15 pages, 104557 bytes) (PDF, 258666 bytes)
A. Pnueli and Y. Kesten. A deductive proof system for CTL*. In Proc. 13th Conference on Concurrency Theory, volume 2421 of Lecture Notes in Computer Science, pages 24-40, Brno, Czech Republic, August 2002. © Springer-Verlag. (Gzipped PostScript, 17 pages, 105358 bytes) (PDF, 249562 bytes)
A. Pnueli, J. Xu, and L. Zuck. Liveness with (0,1,infinity)-counter abstraction. In 14th. International Conference on Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, pages 107-122, Copenhagen, Denmark, July 2002. © Springer-Verlag. (Gzipped PostScript, 18 pages, 132471 bytes)
O. Kupferman, N. Piterman, and M. Vardi. Model checking linear properties of prefix-recognizable systems. In 14th. International Conference on Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, pages 371-385, Copenhagen, Denmark, July 2002. © Springer-Verlag. (Gzipped PostScript, 28 pages, 127382 bytes) (PDF, 272167 bytes)
L. Zuck, A. Pnueli, Y. Fang, B. Goldberg, and Y. Hu. Translation and run-time validation of optimized code. In 2nd Workshop on Runtime Verification, volume 70(4) of Electronic Notes in Theoretical Computer Science, pages 180-201, Copenhagen, Denmark, July 2002. Elsevier Science. (PostScript)
D. Harel, H. Kugler, and R. Marelly. The play-in/play-out approach and tool: Specifying and executing behavioral requirements. In The Israeli Workshop on Programming Languages & Development Environments, Haifa, Israel, July 2002. IBM. (PDF, 173723 bytes)
Y. Koren and D. Harel. A multi-scale algorithm for the linear arrangement problem. In 28th International Workshop on Graph-Theoretic Concepts in Computer Science, volume 2573 of Lecture Notes in Computer Science, pages 293-306, Cesky Krumlov, Czech Republic, June 2002. © Springer-Verlag. (Gzipped PostScript, 14 pages, 112041 bytes) (PDF, 517849 bytes)
D. Harel and Y. Koren. Drawing graphs with non-uniform vertices. In International Working Conference on Advanced Visual Interfaces, Trento, Italy, May 2002. ACM, © ACM. (Gzipped PostScript, 10 pages, 390902 bytes) (PDF, 276946 bytes)
A. Leung, K. V. Palem, and Amir Pnueli. TimeC: A time constraint language for ilp processor compilation. Constraints, 7(2):75-115, April 2002.
D. Harel, H. Kugler, R. Marelly, and A. Pnueli. Smart play-out of behavioral requirements. Technical Report MCS02-08, Weizmann Institute of Science, April 2002. (Gzipped PostScript, 21 pages, 218812 bytes) (PDF, 201050 bytes)
R. Marelly, D. Harel, and H. Kugler. Multiple instances and symbolic variables in executable sequence chart. Technical Report MCS02-05, Weizmann Institute of Science, March 2002. (Gzipped PostScript, 30 pages, 311444 bytes)
D. Harel and H. Kugler. Synthesizing state-based object systems from lsc specifications. International Journal of Foundations of Computer Science, 13(1):5-52, February 2002. (Gzipped PostScript, 47 pages, 178162 bytes) (PDF, 455187 bytes)
Y. Koren and D. Harel. A multi-scale algorithm for the linear arrangement problem. Technical Report MCS02-04, Weizmann Institute of Science, February 2002. (Gzipped PostScript, 26 pages, 366898 bytes) (PDF, 717462 bytes)
L. Zuck, A. Pnueli, and Y. Kesten. Automatic verification of free choice. In Proc. of the 3rd workshop on Verification, Model Checking, and Abstract Interpretation, volume 2294 of Lecture Notes in Computer Science, pages 208-224, Venice, Italy, January 2002. © Springer-Verlag. (Gzipped PostScript, 16 pages, 96771 bytes) (PDF, 259502 bytes)
D. Harel. On the behavior of complex object-oriented systems. In Proceedings Conference on Object-Oriented Modeling of Embedded Real-Time Systems (OMER99 and OMER01), volume P-5 of GI-Edition, Lecture Notes in Informatics series of the German Society of Informatics, pages 11-15, 2002.

2001

D. Harel and Y. Koren. On clustering using random walks. In Proc. 21st conference on Foundations of Software Technology and Theoretical Computer Science, volume 2245 of Lecture Notes in Computer Science, pages 18-41, Bangalore, India, December 2001. © Springer-Verlag. (Springer PDF)
D. Fisman and A. Pnueli. Beyond regular model checking. In Proc. 21st conference on Foundations of Software Technology and Theoretical Computer Science, volume 2245 of Lecture Notes in Computer Science, pages 156-170, Bangalore, India, December 2001. © Springer-Verlag. (Gzipped PostScript, 26 pages, 147781 bytes) (PDF, 349128 bytes)
D. Peled, A. Pnueli, and L. Zuck. From falsification to verification. In Proc. 21st conference on Foundations of Software Technology and Theoretical Computer Science, volume 2245 of Lecture Notes in Computer Science, pages 292-304, Bangalore, India, December 2001. © Springer-Verlag. (Gzipped PostScript, 14 pages, 96769 bytes) (PDF, 220645 bytes)
A. Pnueli, Y. Rodeh, and O. Strichman. Range allocation for equivalence logic. In Proc. 21st conference on Foundations of Software Technology and Theoretical Computer Science, volume 2245 of Lecture Notes in Computer Science, pages 317-333, Bangalore, India, December 2001. © Springer-Verlag. (Gzipped PostScript, 14 pages, 113740 bytes) (PDF, 230343 bytes)
Y. Koren, L. Carmel, and D. Harel. Ace: A fast multiscale eigenvectors computation for drawing huge graphs. Technical Report MCS01-17, Weizmann Institute of Science, December 2001.
N. Kam, D. Harel, and I.R. Cohen. Modeling biological reactivity: Statecharts vs. boolean logic. In Proc. 2nd International Conference on Systems Biology, pages 301-310, Pasadena, CA, USA, November 2001. (PDF, 3968088 bytes)
R. Hadany and D. Harel. A multi-scale algorithm for drawing graphs nicely. Discrete Applied Mathematics, 113(1):3-21, October 2001.
D. Harel, L. Carmel, and D. Lancet. An algorithmic approach to odor communication and reproduction. Technical Report MCS01-16, Weizmann Institute of Science, September 2001.
D. Harel and R. Marelly. Capturing and executing behavioral requirements: The play-in/play-out approach. Technical Report MCS01-15, Weizmann Institute of Science, September 2001. (PDF, 382197 bytes)
O. Shtrichman. Pruning techniques for the bounded model checking problem. In Proc. 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, volume 2144 of Lecture Notes in Computer Science, pages 58-70, Livingston, Scotland, September 2001. © Springer-Verlag. (Gzipped PostScript, 13 pages, 88989 bytes) (PDF, 216548 bytes)
N. Kam, I.R. Cohen, and D. Harel. The immune system as a reactive system: Modeling T-cell activation with statecharts. In Proc. Symposia on Human-Centric Computing Languages and Environments, pages 15-22, Stresa, Italy, September 2001. IEEE, © IEEE Computer Society Press. Won the best paper award. (Gzipped PostScript, 1110784 bytes) (PDF, 144990 bytes)
R. Leviathan and A. Pnueli. Validating software pipelining optimizations. Technical Report MCS01-11, Weizmann Institute of Science, August 2001. (Gzipped PostScript, 13 pages, 108123 bytes) (PDF, 202537 bytes)
L. Zuck, A. Pnueli, and R. Leviathan. Validation of optimizing compilers. Technical Report MCS01-12, Weizmann Institute of Science, August 2001. (Gzipped PostScript, 13 pages, 284260 bytes) (PDF, 320181 bytes)
D. Harel and Y. Koren. Clustering spatial data using random walks. In Proc. 7th ACM International Conference on Knowledge Discovery and Data Mining, pages 281-286, San Francisco, CA, USA, August 2001. ACM, © ACM. (Gzipped PostScript, 21 pages, 1488654 bytes)
O. Kupferman, N. Piterman, and M. Vardi. Extended temporal logic revisited. In 12th International conference on Concurrency theory, volume 2154 of Lecture Notes in Computer Science, pages 519-535, Aalborg, Denmark, August 2001. © Springer-Verlag. (Gzipped PostScript, 17 pages, 128388 bytes) (PDF, 290373 bytes)
N. Piterman and M. Vardi. From bidirectionality to alternation. In 26th International Symposium on Mathematical Foundations of Computer Science, volume 2136 of Lecture Notes in Computer Science, pages 598-610, Marianske Lazne, Czech Republic, August 2001. © Springer-Verlag. (Gzipped PostScript, 16 pages, 67423 bytes) (PDF, 163009 bytes)
W. Damm and D. Harel. Lscs: Breathing life into message sequence charts. Formal Methods in System Design, 19(1):45-80, July 2001. (Kluwer PDF)
T. Arons, A.Pnueli, S.Ruah, J.Xu, and L.Zuck. Parameterized verification with automatically computed inductive assertions. In 13th International Conference on Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 221-234, Paris, France, July 2001. © Springer-Verlag. (Gzipped PostScript, 13 pages, 110152 bytes) (PDF, 294518 bytes)
T. Arons. Using timestamping and history variables to verify sequential consistency. In 13th International Conference on Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 423-425, Paris, France, July 2001. © Springer-Verlag.(Gzipped PostScript, 13 pages, 97523 bytes) (PDF, 236360 bytes) (PVS dump files)
Y. Rodeh and O. Shtrichman. Finite instantiations in equivalence logic with uninterpreted functions. In 13th International Conference on Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 144-154, Paris, France, July 2001. © Springer-Verlag. (Gzipped PostScript, 12 pages, 83574 bytes)
N. Kam, I.R. Cohen, and D. Harel. The immune system as a reactive system: Modeling t-cell activation with statecharts. Technical Report MCS01-09, Weizmann Institute of Science, June 2001. (Gzipped PostScript, 1097295 bytes) (PDF, 295951 bytes)
Y. Koren and D. Harel. Clustering spatial data using random walks. Technical Report MCS01-08, Weizmann Institute of Science, June 2001.
Y. Kesten, A. Pnueli, and M. Vardi. Verification by augmented abstraction : The automata theoretic view. Journal of Computer and System Sciences, 62(4):668-690, June 2001. (Gzipped PostScript, 26 pages, 166116 bytes) (PDF, 3995077 bytes)
A. Pnueli, S. Ruah, and L. Zuck. Automatic deductive verification with invisible invariants. In Tools and Algorithms for the Analysis and Construction of Systems, volume 2031 of Lecture Notes in Computer Science, pages 82-97, Genova, Italy, April 2001. ETAPS, © Springer. (Gzipped PostScript, 16 pages, 110084 bytes) (PDF, 265592 bytes)
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. Theoretical Computer Science, 256:93-112, April 2001. (Gzipped PostScript, 25 pages, 136882 bytes) (PDF, 296508 bytes)
A. Pnueli, Y. Rodeh, and O. Strichman. Finite instantiations in equivalence logic with uninterpreted functions. Technical report, Weizmann Institute of Science, 2001. (Gzipped PostScript, 22 pages, 118008 bytes) (PDF, 272518 bytes)
Y. Kesten, A. Pnueli, L Raviv, and E. Shahar. Model checking with strong fairness. Technical report MCS01-07, Weizmann Institute of Science, March 2001. (Gzipped PostScript, 24 pages, 141016 bytes) (PDF, 325553 bytes)
L. Carmel, D. Harel, and D. Lancet. Estimating the size of the olfactory repertoire. Technical Report MCS01-06, Weizmann Institute of Science, February 2001.
T. Arons and A. Pnueli. A methodology for deductive verification of out-of-order execution systems based on predicted values. Technical Report MCS01-04, Weizmann Institute of Science, February 2001. (Gzipped PostScript, 16 pages, 94456 bytes)
A. Leung, K. Palem, and A. Pnueli. Scheduling time-constrained instructions on pipelined processors. ACM Transactions on Programming Languages and Systems, 23(1):73-103, January 2001. (PostScript)
D. Harel. From play-in scenarios to code: An achievable dream. IEEE Computer, 34(1):53-60, january 2001. (IEEE PDF)

2000

E. Sedletsky, A. Pnueli, and M. Ben-Ari. Formal verification of the ricart-agrawala algorithm. In Proc. 20th Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lecture Notes in Computer Science, pages 325-335. © Springer-Verlag, December 2000. (PDF, 188124 bytes)
O. Kupferman, N. Piterman, and M.Y. Vardi. Fair equivalence relations. In Proc. 20th Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lecture Notes in Computer Science, pages 151-163, © Springer-Verlag, December 2000. (Gzipped PostScript, 12 pages, 50159 bytes) (PDF, 124352 bytes)
D. Harel and Y. Koren. A fast multi-scale method for drawing large graphs. In 8th International Symposium on Graph Drawing, volume 1984 of Lecture Notes in Computer Science, pages 183-196, Williamsburg, VA, USA, September 2000. © Springer-Verlag. (Gzipped PostScript, 14 pages, 1037499 bytes)
D. Harel and O. Kupferman. On the behavioral inheritance of state-based objects. In Proc. 34th International Confefence on Component and Object Technology, Santa Barbara, CA, USA, August 2000. IEEE, IEEE Computer Society. (Zipped PostScript)
D. Harel and B. Rumpe. Modeling languages: Syntax, semantics and all that stuff, part i: The basic stuff. Technical Report MCS00-16, Weizmann Institute of Science, August 2000.
D. Harel and H. Kugler. From Scenarios to Automata to Code: On the Future of System Development. In 5th Int. Conf. on Implementation and Application of Automata, volume 2088 of Lecture Notes in Computer Science, © Springer-Verlag, London, Ontario, Canada, July 2000. (Full Version)
A. Pnueli and E. Shahar. Liveness and acceleration in parameterized verification. In Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 328-343. © Springer-Verlag, July 2000. (Gzipped PostScript, 16 pages, 100687 bytes) (PDF, 241435 bytes)
Y. Kesten, Z. Manna, and A. Pnueli. Verification of clocked and hybrid systems. Acta Informatica, 36(11):836-912, 2000. (Gzipped PostScript, 74 pages, 271058 bytes) (PDF, 10902198 bytes)
O. Shtrichman. Tuning sat checkers for bounded model-checking. In Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 480-494. © Springer-Verlag, July 2000. (Gzipped PostScript, 15 pages, 103475 bytes) (PDF, 249073 bytes)
E. Asarin, O. Bournez, T. Dang, O. Maler, and A. Pnueli. Effective synthesis of switching controllers for linear systems. Proceedings of the IEEE, 88(7):1011-1025, July 2000. (PDF)
D. Harel and G. Yashchin. An algorithm for blob hierarchy layout. Technical Report CS99-09, Weizmann Institute of Science, May 1999.
D. Harel and G. Yashchin. An algorithm for blob hierarchy layout. In Proc. Working Conference on Advanced Visual Interfaces, pages 29-40, Palermo, Italy, May 2000. ACM Press.
D. Harel and Y. Koren. Drawing graphs with non-uniform vertices. Technical Report MCS00-09, Weizmann Institute of Science, April 2000.
Y. Kesten and A. Pnueli. Control and data abstractions: The cornerstones of formal verification. International Journal on Software Tools for Technology Transfer (STTT), 2(1):328-342, 2000. (Gzipped PostScript, 40 pages, 204861 bytes) (PDF, 6476972 bytes)
T. Arons and A. Pnueli. A comparison of two verification methods for speculative instruction execution. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), number 1785 in Lecture Notes in Computer Science, pages 487-502, Berlin, Germany, March 2000. © Springer-Verlag. (Gzipped PostScript, 15 pages, 89001 bytes) (PDF, 220148 bytes) (PVS dump files)
Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, 163, 2000. (Gzipped PostScript, 17 pages, 164467 bytes) (PDF, 4364642 bytes)
A. Pnueli, O. Shtrichman, and M. Siegel. Translation validation: From signal to c. In Correct System Design Recent Insights and Advances, volume 1710 of Lecture Notes in Computer Science, pages 231-255. © Springer, March 2000. (Gzipped PostScript, 25 pages, 129250 bytes) (PDF, 302749 bytes)
Harel. From play-in scenarios to code: An achievable dream . In Proc. International Conference on Fundamental Approaches to Software Engineering, volume 1783 of Lecture Notes in Computer Science, pages 22-34. Springer-Verlag, March 2000. (Springer PDF)
D. Harel. From play-in scenarios to code: An achievable dream. Technical Report MCS00-06, Weizmann Institute of Science, February 2000.
O. Lichtenstein and A. Pnueli. Propositional temporal logics: Decidability and completeness. Logic Journal of the IGPL, 8(1):55-85, 2000. (Gzipped PostScript, 31 pages, 146539 bytes)

1999

K. Altisen, G. Gossler, A. Pnueli, J. Sifakis, S. Tripakis, and S. Yovine. A framework for scheduler synthesis. In Proc. 20th IEEE Real-Time Systems Symposium, pages 154-163, Phoenix, AZ, USA, December 1999. IEEE, IEEE Computer Society Press. (IEEE PDF)
D. Harel and Y. Koren. A fast multi-scale method for drawing large graphs. Technical Report MCS99-21, Weizmann Institute of Science, November 1999.
D. Harel and H. Kugler. Synthesizing state-based object systems from lsc specifications. Technical Report MCS99-20, Weizmann Institute of Science, October 1999.
Y. Kesten and A. Pnueli. Verifying liveness by augmented abstraction. In Computer Science Logic, 13th International Workshop, volume 1683 of Lecture Notes in Computer Science, pages 141-156. © Springer-Verlag, September 1999. (Gzipped PostScript) (PDF)
A. Pnueli. Deduction is forever. An invited talk at "Formal Methods", Toulouse, September 1999.
Y. Kesten, A. Klein, A. Pnueli, and G. Raanan. A perfecto verification: Combining model checking with deductive analysis to verify real-life software. In Formal Methods, Volume I, volume 1708 of Lecture Notes in Computer Science , pages 173-194, Toulouse, France, September 1999. © Springer-Verlag. (Springer PDF)
Y. Kesten, A. Klein, A. Pnueli, and G. Raanan. Bridging the e-business gap through formal verification. In M. Hinchey and J. Bowen, editors, Industrial-Strength Formal Methods in Practice, Formal Approaches to Computing and Information Technology, chapter 6, pages 117-137. © Springer-Verlag, September 1999.
D. Harel and M. Kaminsky. Strengthened results on nonregular pdl. Technical Report MCS99-13, Weizmann Institute of Science, August 1999.
A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small domains instantiations. In Proc. 11th International Computer Aided Verification Conference, volume 1633 of Lecture Notes in Computer Science , pages 455-469. © Springer-Verlag, July 1999. (Gzipped PostScript, 12 pages, 102355 bytes)
B. Jonsson, A. Pnueli, and C. Rump. Proving refinement using transduction. Distributed Computing, 12(2-3):129-149, June 1999. (Springer PDF)
D. Harel and O. Kupferman. On the behavioral inheritance of state-based objects. Technical Report MCS99-12, Weizmann Institute of Science, June 1999.
R. Hadany and D. Harel. Multi-scale algorithm for drawing graphs nicely. In 25th International Workshop on Graph-Theoretic Concepts in Computer Science, volume 1665 of Lecture Notes in Computer Science, pages 262-277, Ascona, Switzerland, June 1999. Springer-Verlag. (Springer PDF)
Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Decidable integration graphs. Information and Computation, 150(2):209-243, May 1999. (I&C PDF)
W. Damm and D. Harel. Lscs: Breathing life into message sequence charts. Technical Report CS98-09, Weizmann Institute of Science, May 1998.
O. Bournez, O. Maler, and A. Pnueli. Orthogonal polyhedra: Representation and computation. In 2nd International Workshop on Hybrid Systems: Computation and Control, volume 1569 of Lecture Notes in Computer Science , Berg en Dal, The Netherlands, March 1999. © Springer-Verlag. (Springer PDF)
W. Damm and D. Harel. Lscs: Breathing life into message sequence charts. In Proc. 3rd international Conferene on Formal Methods for Open Object-Based Distributed System, volume 139 of IFIP, pages 293-312, Florence, Italy, February 1999. International Federation for Information Processing, Kluwer Academic Publishers.
T. Arons and A. Pnueli. Verifying Tomasulo's algorithm by refinement. In The Twelfth International Conference on VLSI Design, pages 306-309, Goa, India, January 1999. IEEE Computer Society. (Gzipped PostScript, 4 pages, 25211 bytes) (PVS dump file)
J. Gal-Ezer and D. Harel. Curriculum and course syllabi for a high-school program in computer science. Computer Science Education, 9(2):114-147, 1999.
J. Gal-Ezer and D. Harel. Curriculum and course syllabi for a high-school program in computer science. Technical Report CS99-02, Weizmann Institute of Science, January 1999.
R. Hadany and D. Harel. A multi-scale algorithm for drawing graphs nicely. Technical Report CS99-01, Weizmann Institute of Science, January 1999.

1998

A. Pnueli and T. Arons. Verification of data-insensitive circuits: An in-order-retirement case study. In Formal Methods in Computer-Aided Design (FMCAD '98), volume 1522 of Lecture Notes in Computer Science , pages 351-368, Palo Alto, CA, November 1998. © Springer-Verlag. (Gzipped PostScript, 18 pages, 102959 bytes) (PVS dump file)
A. Pnueli, O. Shtrichman, and M. Siegel. Translation validation: From dc+ to c*. In International Workshop on Current Trends in Applied Formal Methods, volume 1641 of Lecture Notes in Computer Science, pages 137-150, Boppard, Germany, October 1998. © Springer-Verlag.
J. Gal-Ezer and D. Harel. What (else) should cs educators know. Communications of the ACM, 41(9):77-84, September 1998.
W. Damm, A. Pnueli, and S. Ruah. Herbrand automata for hardware verification. In 9th International Conference on Concurrency Theory, volume 1466 of Lecture Notes in Computer Science , pages 67-83, Nice, France, September 1998. © Springer-Verlag. (Gzipped PostScript, 17 pages, 72100 bytes)
E. Asarin, O. Maler, and A. Pnueli. On discretization of delays in timed automata and digital circuits. In Proc. 9th International Conference on Concurrency Theory, volume 1466 of Lecture Notes in Computer Science, pages 470-484, Nice, France, September 1998. © Springer-Verlag. (PostScript)
W. Damm, B. Josko, H. Hungar, and A. Pnueli. A compositional real-time semantics of STATEMATE designs. In International Symposium Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science , pages 186-238, Bad Malente, Germany, September 1998. © Springer-Verlag. (Springer PDF)
Y. Kesten and A. Pnueli. Modularization and abstraction: The keys to formal verification. In Proc. 23rd International Symposium Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, pages 54-71, Brno, Czech Republic, August 1998. © Springer-Verlag. (Gzipped PostScript) (Springer PDF)
Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. In Proc. 25th International Colloquium on Automata, Languages, and Programming, volume 1443 of Lecture Notes in Computer Science , pages 1-16, Aalborg, Denmark, July 1998. © Springer-Verlag. (Gzipped PostScript) (PDF)
A. Pnueli, M. Siegel, and O. Shtrichman. Translation validation for synchronous languages. In Proc. 25th International Colloquium on Automata, Languages, and Programming, volume 1443 of Lecture Notes in Computer Science , pages 235-246, Aalborg, Denmark, July 1998. © Springer-Verlag. (Gzipped PostScript, 12 pages, 62428 bytes)
A. Pnueli, M. Siegel, and O. Shtrichman. The code validation tool (cvt) - automatic verification of code generated from synchronous languages. In Proc. of the intl. workshop of Software Tools for Technology Transfer, volume NS-98-4 of BRICS notes series, pages 7-12, Aalborg, Denmark, July 1998. BRICS. (Gzipped PostScript, 106710 bytes)
A. Pnueli. Deductive vs. model-theoretic approaches to formal verification. In Proceedings of the 15th International Conference on Automated Deduction (CADE-98), volume 1421 of LNAI, pages 301-301, Berlin, July 1998. Springer-Verlag.
A. Pnueli, E. Asarin, O. Maler, and J.Sifakis. Controller synthesis for timed automata. In 5th IFAC conference on System Structure and Control, IFAC Proceedings Volumes, pages 469-474, Nantes, France, July 1998. IFAC, Elsevier.
D. Harel and M. Sardas. An algorithm for straight-line drawing of planar graphs. Algorithmica, 20(2):119-135, February 1998. (Springer PDF)
A. Pnueli, O. Shtrichman, and M. Siegel. The code validation tool cvt: Automatic verification of a compilation process. International Journal on Software Tools for Technology Transfer (STTT), 2(1):192-201, 1998. (Gzipped PostScript, 10 pages, 127055 bytes)