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