Publications 2002
Follow paper's title for abstract
Link's may lead to sites with restricted access
- 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 2nd 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.