[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Zhong Shao
- Certified Software
- Commun ACM V53n12(Dec 2010)pp56-66
[ 1859204.1859226 ]
- =IDEAS DEPENDABLE CORRECT PROOF CHECKER ASSEMBLER MACHINE CODE TOOLS EXAMPLES Coq METALOGIC FUNCTIONAL NONSEQUENTIAL
- Minimize the components that can damage the dependability of the system.
- Both proofs and specifications can be represented by executable programs. Example using CoQ
- (Wikipedia)|-Coq implements a dependently typed functional programming language...
[ en.wikipedia.org/wiki/Coq ]
- "huge cost in constructing ... specifications and proofs"
- Dynamic validation - add a check after an unproved step and use a proved component if the check fails.
- "time to market is likely terrible"
- PCC - proof-carrying code - give executable code with a proof of safety to a host that checks the proof.
- Proof checking is automated and about as difficult as type checking.
- FPCC - Foundational PCC.
- CAP - certified assembly programming - using a mechanisable Metalogic.
- Modular reasoning. Separation logics. CSL - concurrent separation logic.
- Domain specific logics.
- There exist certified garbage collectors, thread libraries, compilers, and certifying compilers,
- (dick)|-How to handle changing requirements and specifications? Can proofs be agile?
Search for bibliographic items containing a matching string.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]