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