Quote: Euclid's algorithm for greatest common divisor; with proof [»eucl_300, OK]

Quote: geometric construction of equilateral triangles; with proof [»eucl_300, OK]

Quote: rigorous, detailed, readable specification from real-world traces of three implementations of the TCP/IP protocols and Sockets API; verified with a symbolic model checker [»bishS1_2006]

Quote: a program and its proof should be developed together; with the proof usually leading the way [»grieD_1981]

Quote: formality is important in programming because of the large amount of detail which must be absolutely correct [»grieD_1981]

Quote: instead of program verification should derive correct programs with correctness checked at each stage [»scheWL9_1983]

Quote: should develop program and its correctness proof together [»mannZ7_1979]

Quote: correctness proof and program should be written together [»dijkEW10_1972]

Quote: must develop a program and its correctness proof together; better to derive a correct program than to have a direct correctness proof [»baueFL_1976]

Quote: writing new code is natural with reference immutability; helped define interfaces; easier than annotating existing code [»birkA10_2004]

Quote: describe a routine accurately; include preconditions, postconditions, validity conditions, accuracy, time taken, and method [»turiA3_1951]

Quote: verification gives programmers a language for understanding the program as it is written; important explanations become assertions [»bentJ10_1983]

Quote: formal semantics enables compile-time optimization, analysis, and verification

Quote: write programs as a specification in first-order predicate calculus and incrementally refine it into a program [»hehnEC2_1984]

Quote: it is more natural to describe a program by its derivation or evolution from specifications [»scheWL9_1983]

Quote: every program is a transition axiom specification; a compiler translates the program's explicit and implicit state functions [»lampL1_1989]

Quote: a programmer should make assertions that imply a correct routine; then checking the assertions checks the routine [»turiAM6_1949]

Quote: assist a program checker with a table of assertions for each state of the machine with restrictions on the induction variables, and the next states [»turiAM6_1949]

Quote: SD3 trust management computes answer and verified proof together; only certified evaluator in trusted computing base; e.g., a secure name service [»jimT5_2000]

Quote: a verification model must identify control states, event types, and event responses as code fragments [»holzGJ5_1999]

Quote: a program includes global, local, and induction variables; only local and induction (the bound variables) may use shared storage; [»goldHH_1948, OK]

Quote: it is important to find the loop invariant for each loop [»grieD_1981]