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

Bibliographic Item (1.0)

Shao10

  1. Zhong Shao
  2. Certified Software
  3. Commun ACM V53n12(Dec 2010)pp56-66 [ 1859204.1859226 ]
  4. =IDEAS DEPENDABLE CORRECT PROOF CHECKER ASSEMBLER MACHINE CODE TOOLS EXAMPLES Coq METALOGIC FUNCTIONAL NONSEQUENTIAL
  5. Minimize the components that can damage the dependability of the system.
  6. Both proofs and specifications can be represented by executable programs. Example using CoQ
  7. (Wikipedia)|-Coq implements a dependently typed functional programming language... [ en.wikipedia.org/wiki/Coq ]
  8. "huge cost in constructing ... specifications and proofs"
  9. Dynamic validation - add a check after an unproved step and use a proved component if the check fails.
  10. "time to market is likely terrible"
  11. PCC - proof-carrying code - give executable code with a proof of safety to a host that checks the proof.
  12. Proof checking is automated and about as difficult as type checking.
  13. FPCC - Foundational PCC.
  14. CAP - certified assembly programming - using a mechanisable Metalogic.
  15. Modular reasoning. Separation logics. CSL - concurrent separation logic.
  16. Domain specific logics.
  17. There exist certified garbage collectors, thread libraries, compilers, and certifying compilers, etc.
  18. (dick)|-How to handle changing requirements and specifications? Can proofs be agile?

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]