| [1] | Tamarah Arons and Amir Pnueli.
A comparison of two verification methods for speculative instruction
execution.
In Susanne Graf and Michael Schwartzbach, editors, 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. |
| [2] | Roel Bloo, Jozef Hooman, and Edwin de Jong.
Semantical aspects of an architecture for distributed embedded
systems.
In Proceedings of the 2000 ACM Symposium on Applied Computing
(SAC 2000), volume 1, pages 149-155, Como, Italy, March 2000. Association
for Computing Machinery. More information and full paper available here |
| [3] | Victor Carreño and César Muñoz.
Aircraft trajectory modeling and alerting algorithm verification.
In Mark Aargaard and John Harrison, editors, Theorem Proving in
Higher Order Logics: 13th International Conference, TPHOLs 2000, volume
1869 of Lecture Notes in Computer Science, pages 90-105, Portland, OR,
August 2000. Springer-Verlag. More information and full paper available here |
| [4] | Victor Carreño and César Muñoz.
Formal analysis of parallel landing scenarios.
In 19th AIAA/IEEE Digital Avionics Systems Conference,
Philadelphia, PA, October 2000. |
| [5] | Dmitri Chkliaev, Jozef Hooman, and Peter van der Stok.
Mechanical verification of transaction processing systems.
In Third International Conference on Formal Engineering Methods
(ICFEM 2000), pages 89-97, York, England, November 200. IEEE Computer
Society. More information and full paper available here |
| [6] | James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn
Laubach, and Hongjun Zheng.
Bandera: Extracting finite-state models from Java source code.
In 22nd International Conference on Software Engineering, pages
439-448, Limerick, Ireland, June 2000. IEEE Computer Society. Compressed PS |
| [7] | Edwin de Jong, Jaco van de Pol, and Jozef Hooman.
Refinement in requirements specification and analysis: A case study.
In 7th IEEE International Conference and Workshop on the
Engineering of Computer Based Systems (ECBS), pages 290-298, Edinburgh,
Scotland, April 2000. IEEE Computer Society. More information and full paper available here |
| [8] | Marco Devillers, David Griffioen, Judi Romijn, and Frits Vaandrager.
Verification of a leader election protocol: Formal methods applied to
IEEE 1394.
Formal Methods in Systems Design, 16(3):307-320, June 2000. |
| [9] | J. Ford and I. A. Mason.
Operational techniques in PVS-a preliminary evaluation.
In Proceedings of the Australasian Theory Symposium, CATS
'01, Gold Coast, Queensland, Australia, January-February 2001. More information and full paper available here |
| [10] | Angelo Gargantini and Elvinia Riccobene.
Encoding Abstract State Machines in PVS.
In Yuri Gurevich, Phillip W. Kutter, Martin Odersky, and Lothar
Thiele, editors, Abstract State Machines: Theory and Applications (ASM
2000), number 1912 in Lecture Notes in Computer Science, pages 303-322,
Monte Verità, Switzerland, March 2000. Springer-Verlag. More information and full paper available here |
| [11] | Hanne Gottliebsen.
Transcendental functions and continuity checking in PVS.
In Mark Aargaard and John Harrison, editors, Theorem Proving in
Higher Order Logics: 13th International Conference, TPHOLs 2000, volume
1869 of Lecture Notes in Computer Science, pages 197-214, Portland,
OR, August 2000. Springer-Verlag. PS |
| [12] | Marieke Huisman and Bart Jacobs.
Inheritance in higher order logic: Modeling and reasoning.
In Mark Aargaard and John Harrison, editors, Theorem Proving in
Higher Order Logics: 13th International Conference, TPHOLs 2000, volume
1869 of Lecture Notes in Computer Science, pages 301-319, Portland,
OR, August 2000. Springer-Verlag. Compressed PS |
| [13] | Marieke Huisman and Bart Jacobs.
Java program verfication via a hoare logic with abrupt termination.
In Tom Maibaum, editor, Fundamental Approaches to Software
Engineering, FASE 2000, number 1783 in Lecture Notes in Computer Science,
pages 284-303, Berlin, Germany, March/April 2000. Springer-Verlag. Compressed PS |
| [14] | Paul Jackson.
Total-correctness refinement for sequential reactive systems.
In Mark Aargaard and John Harrison, editors, Theorem Proving in
Higher Order Logics: 13th International Conference, TPHOLs 2000, volume
1869 of Lecture Notes in Computer Science, pages 320-337, Portland,
OR, August 2000. Springer-Verlag. Compressed PS |
| [15] | Paul Kolano, Richard Kemmerer, and Dino Mandrioli.
Parallel refinement mechanisms for real-time systems.
In Tom Maibaum, editor, Fundamental Approaches to Software
Engineering, FASE 2000, number 1783 in Lecture Notes in Computer Science,
pages 35-50, Berlin, Germany, March/April 2000. Springer-Verlag. |
| [16] | Nazanin Mansouri and Ranga Vemuri.
Automated correctness condition generation for formal verification of
synthesized RTL designs.
Formal Methods in Systems Design, 16(1):59-91, January 2000. |
| [17] | Abdel Mokkedem, Ravi M. Hosabettu, Michael D. Jones, and Ganesh C.
Gopalakrishnan.
Formalization and analysis of a solution to the PCI 2.1 bus
transaction ordering problem.
Formal Methods in Systems Design, 16(1):93-119, January 2000. Compressed PS |
| [18] | Abdel Mokkedem and Tim Leonard.
Formal verification of the Alpha 21364 network protocol.
In Mark Aargaard and John Harrison, editors, Theorem Proving in
Higher Order Logics: 13th International Conference, TPHOLs 2000, volume
1869 of Lecture Notes in Computer Science, pages 443-461, Portland,
OR, August 2000. Springer-Verlag. |
| [19] | Holger Pfeifer.
Formal verification of the TTA group membership algorithm.
In Tommaso Bolognesi and Diego Latella, editors, Formal
Description Techniques and Protocol Specification, Testing and Verification
FORTE XIII/PSTV XX 2000, pages 3-18, Pisa, Italy, October 2000. Kluwer
Academic Publishers. More information and full paper available here |
| [20] | Michaël Rusinowitch, Sorin Stratulat, and Francis Klay.
Mechanical verification of a generic incremental ABR conformance
algorithm.
In E. A. Emerson and A. P. Sistla, editors, Computer-Aided
Verification, CAV '2000, volume 1855 of Lecture Notes in Computer
Science, pages 344-357, Chicago, IL, July 2000. Springer-Verlag. |
| [21] | V. Rusu, L. du Bousquet, and T. Jéron.
An approach to symbolic test generation.
In 2nd International Workshop on Integrated Formal Method
(IFM'00), number 1945 in Lecture Notes in Computer Science, pages 338-357,
Dagstuhl, Germany, November 2000. Springer-Verlag. PS |
| [22] | Joachim van den Berg, Marieke Huisman, Bart Jacobs, and Erik Poll.
A type-theoretic memory model for verification of sequential Java
programs.
In Didier Bert, Christine Choppy, and Peter Mosses, editors,
Recent Trends in Algebraic Development Techniques, WADT '99, number 1827
in Lecture Notes in Computer Science, pages 1-21, Toulouse, France,
September 1999. Springer-Verlag. |