The Case for Formal Verification (2013)

Re:The Case for Formal Verification (2013) by dkarapetyan on Sunday April 20, 2014 @07:28PM (#7618874)

What exactly is doing the verification? Another program, no? In which case why would you trust that program any more than the compiler that generated the machine code? At some point you must trust something to be correct. Whether that's the compiler or something else doesn't really change anything.

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by vilhelm_s on Sunday April 20, 2014 @09:06PM (#7619158)

The idea is to minimize the trusted computing base---a compiler and runtime system for a high level language is a big and complicated system, so it is very hard to get it right, but a proof checker can be small so it is easier to be confident that it is correct. (This idea is also known as the "de Bruijn criterion").

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by dllthomas on Monday April 21, 2014 @05:05AM (#7620343)

Ideally, we should minimize the code in any given path to assurance, but maximize the number of independent paths to assurance (modulo resource constraints).

[ Parent | on HN ]