Abstract
Formal analysis remains outside the mainstream of system design practice. Interactive methods and tools are regarded by some to be on the margin of useful research in this area. Although it may seem relatively academic to some, it is vital that this the so-called “theorem proving approach” continue to be as vigorously explored as approaches favoring highly automated reasoning. Design derivation, a term for design formalisms based on transformations and equivalence, represents just a small twig on the theorem-proving branch of formal system analysis. A perspective on current trends is presented from this remote outpost, including a review of the author’s work since the early 1980s.
Work described in this paper was supported by the National Science Foundation under grants MIP8707067, MIP8921842, MIP9208745, and MIP9610358.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Jon Barwise and Lawrence Moss. Vicious Circles. CLSI Publications, Stanford, California, 1996.
Carl B. Boyer. The History of the Calculus and its Conceptual Development. Dover, New York, 1959. Republished 1949 edition.
Joshua D. Guttman, John D. Ramsdell, and Mitchell Wand. VLISP: a verified implementation of Scheme. Lisp and Symbolic Computation, 8:5–32, 1995.
C. A. R. Hoare. Theories of programming: Top-down and bottom-up meeting in the middle. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, FM’99-Formal Methods. LNCS 1708.
A. J. C. Hurkens, Monica McArthur, Yiannis M. Moschovakis, Lawrence S. Moss, and Glen T. Whitney. The logic of recursive equations. The Journal of Symbolic Logic, 63(2):451–478, June 1998.
Steven D. Johnson. The Indiana University System Design Methods Laboratory home page. http://www.cs.indiana.edu/hmg/hmg.html.
Steven D. Johnson. Manipulating logical organization with system factorizations. In M. Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, pages 260–281. LNCS 408, 1989.
Steven D. Johnson. A workshop on formal methods education: an aggregation of opinions. International Journal on Software Tools for Technology Transfer, 2(3):203–207, November 1999.
Steven D. Johnson and Paul S. Miner. Integrated reasoning support in system design: design derivation and theorem proving. In Hon F. Li and David K. Probst, editors, Advances in Hardware Design and Verification (CHARME’97), pages 255–272. Chapman-Hall, 1997.
Lawrence S. Moss. Recursion and corecursion have the same equational logic. Theoretical Computer Science, to appear in 2002. http://math.indiana.edu/home/moss/home.html.
Amir Pnueli. These quotations are extracted from transparencies for invited talks at PODC’90, FM’99, and CAV’00. They can be found at http://www.wisdom.weizmann.ac.il/amir/invited-talks.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Johnson, S.D. (2001). View from the Fringe of the Fringe. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_1
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive