rw-book-cover

Highlights

  • method for automatically generating mathematical proofs to verify software correctness (View Highlight)
  • The technique, known as machine-checking, involves creating a proof that the software performs as expected, and then using a theorem prover to confirm the proof’s accuracy. (View Highlight)
  • writing these proofs has been a laborious task, requiring extensive expertise and often resulting in proofs longer than the software code itself. (View Highlight)