Advertisement

View from the Fringe of the Fringe

Extended Summary
  • Steven D. Johnson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)

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.

Keywords

Model Checker Formal Method Theorem Prove Recursive Equation Proof Assistant 
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

  1. 1.
    Jon Barwise and Lawrence Moss. Vicious Circles. CLSI Publications, Stanford, California, 1996.zbMATHGoogle Scholar
  2. 2.
    Carl B. Boyer. The History of the Calculus and its Conceptual Development. Dover, New York, 1959. Republished 1949 edition.zbMATHGoogle Scholar
  3. 3.
    Joshua D. Guttman, John D. Ramsdell, and Mitchell Wand. VLISP: a verified implementation of Scheme. Lisp and Symbolic Computation, 8:5–32, 1995.CrossRefGoogle Scholar
  4. 4.
    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.CrossRefGoogle Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    Steven D. Johnson. The Indiana University System Design Methods Laboratory home page. http://www.cs.indiana.edu/hmg/hmg.html.
  7. 7.
    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.Google Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.
  11. 11.
    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.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Steven D. Johnson
    • 1
  1. 1.Indiana University Computer Science DepartmentIndia

Personalised recommendations