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