[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)


  1. Sam Owe & John Rushby & Natarajan Shankar & Friedrich von Henke
  2. Formal Verification for Fault-Tolerant architectures: prolegomena to the Design of PVS
  3. IEEE Trans on Software Eng VSE-21n2(Feb 1995)pp107-125
  5. PVS::= See http://www.csl.sri.com/pvs.html, System for generating proofs.
      PVS next generation after EHDM(1984)


      uses ASCII input plus map to LaTeX and graphics, under EMACS ftp://ftp.csl.sri.com/pub/pvs

      Application to concurrent faulty systems.

      p114: "Most of the proofs ... not to mention many of the theorems and some of the algorithms wer incorrect when we started... our axiomatizations were occassionally unsound, and sometimes they were sound but did not say what we thought they did... our verifiactions are seldom finished: changed assumptions and requirements, the desire to improve an argument or a bound, and simple experiementation, have led us to revise some or all of our verifiactions several times... [they are used] by someone other than their original developer.....structured....modular"

      "we found that substantial effort was expended on the formal development of 'background theories' such as summations, bitvectors, finite sets, and so on. Clearly, it is necessary that such theories should be made available in libraries for future reuse."

      Help in debugging specifications.

      working(r):set[R]={r | member(c, OK(r))}.

      p118: "Some specification environments allow specifications to be expressed directly in terms of mathematical symbols[...]we have found that the burden of supporting these conveniences outway the benefits, bringing in the wake such menaces to productivity as structure editors, and a plethora of mouse and menu selections. In the US, at least, most scientists and engineers are fast touch typists, and we ind a conventional program editor provides a more productive environment for rapid interaction than a graphical user interface[...]LaTeX,...graphical representation of module dependencies and proof trees...hypertext"

Search for bibliographic items containing a matching string.

(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.

To see the complete bibliography (1Mb+) select:[Bibliography]