Quote: the proper product of programming is arguments that a program is a trustworthy solution [»dijkEW_1982]

Quote: correct code by using sound principles during design, verification by analysis, and exhaustive testing of small cases [»bentJ10_1983]

Quote: discussion of importance of formal proofs for proving programs [»merrG12_1983, OK]

Quote: design one language feature at a time; improvement, efficient, documentation, security, examples, proof rule [»hoarCA_1974]

Quote: errors and oversights are likely when preparing tabular, mathematical descriptions of functions; need many proofs of "obviously true" theorems [»parnDL8_1993]

QuoteRef: dijkEW10_1972 ;;864 should be able to prove programs true

QuoteRef: dijkEW_1979 ;;445 "we must be able to discuss correctness independently of any underlying computational model [i.e. questions of efficiency]

Quote: if we have complete source code then the correctness of a system is completely knowable [»weisM11_1987]

Quote: create a abstract program or program schema by removing data typing and function definition [»elspB6_1972]

Quote: without a formal semantics or a formal type system, can not reason about Java or the security properties of its libraries [»deanD5_1996]

Quote: spec-types have different representations but the same set of operators; operators are generic [»parnDL3_1976]

Quote: if can prove a program correct according to its specifications, can then replace spec-types with other variables of the same type, but different modes

Quote: reason about programs in terms of mathematical domains; e.g., 'string of integers' for a stack or queue, not its concrete representation [»harmDE5_1991]

Quote: need to prove correspondence between sequential composition structure of a program and its conjunctively structured specification [»hoarCA9_1987]

Quote: in formal methods there is an unreasonable focus on proof of correctness; in other areas, engineers use mathematics to derive important properties such as the maximum voltage between two terminals [»parnDL4_1996]

Quote: designers of safety-critical systems must convince themselves, the customer, and certification authorities that the design and implementation are correct

Quote: can analyze an electrical circuit via mathematical equations [»parnDL10_1976]

Quote: need a mathematical science of computation to prove that programs meet their specifications; check the proofs by computer

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: model checking is automated, symbolic testing for properties expressed in temporal logic; can handle 10^100 states [»thomS4_2000]

Quote: a model checker produces a system trace that failed a particular property; particularly useful to diagnosing problems [»thomS4_2000]

Quote: use SPIN for design and verification of asynchronous process systems using rendezvous, buffered channels, and/or shared variables; design with PROMELA [»holzGJ5_1997]

Quote: SPIN represents correctness claims in linear temporal logic (LTL)

Quote: sequential execution is function composition; a neat, simple model with deterministic results [»leeEA5_2006]

Quote: write a detailed, hierarchical proof with a preamble that describes assumptions and why the desired conclusion implies the result [»abadM1_1993]

Quote: a program is correct if it is correct when each part is correct, and if each part is correct [»parnDL12_1994]

Quote: Larch divides a specification into mathematical abstractions and program interfaces [»birrAD_1991a]

Quote: type systems do more than any other formal method to ensure correctness; constrains interface; ensures compatibility [»leeEA9_2000]

Quote: use related field analysis to remove 50% of array bounds checks; proves relationships between fields of an object [»aggaA6_2001]

Quote: can simplify problem if formal verification is used for finding bugs instead of proving correctness; e.g., check cache-coherence protocol with four processors, one cache line, and two data values [»dillDL4_1996]

Quote: mentally verify clear boxes by verifying a small number of correctness conditions; can check unanimously in a few seconds [»lingRC5_1993]

Quote: test data may suggest a simple strategy for proving programs correct [»gellM5_1978]

Quote: prove that program satisfies a specification by proving that a combined program never calls the error function; insert the specification whereever its pattern is triggered [»cookB1_2007]

Quote: prove microcode program via an APL-like symbolic simulation on bit arrays; symbolic theorems and tests matched to actual [»cartWC_1978, OK]

Quote: with reduction languages, can derive proofs in terms of the algebra instead of a separate logical system [»backJ8_1978a]

Quote: confirm that a program implements an intended function by correctness conditions for sequence, alternation, and iteration [»lingRC5_1993]

Quote: refinement naming convention allows a new verification technique

Quote: verify large programs in terms of sets, functions, stacks and queues; not arrays and programs [»millHD9_1987]

Quote: NIL limits side-effects by erroneous programs to inappropriate results of the correct type; by typestate checking [»stroRE5_1985]

Quote: proof that document D is the object that client C associates with name N; by transitivity, signed certificates, and hashes [»howeJ_2000]

Quote: certified evaluation via a proof checker for lists of facts, security rules, and derivations; 100 lines of code [»jimT5_2000]

Quote: programmers and implementers use the formal specification of Modula-3 threads [»birrAD_1991a]

Quote: an untrained user found an error in the formal specification of Modula-3 threads; another error was missed for a year

Quote: proof of type soundness for a large, sequential sublanguage of Java; via the interactive theorem prover Isabelle/HOL [»nipkT1_1998]

Quote: wrote 20 thousand line program without arrays; used verification instead of unit testing; no errors after installation [»millHD2_1986]

Quote: using principles of safe programming, constructed an 8000 line assembly program without error [»andeT_1985]

Quote: used assertions to improve the reliability and correctness of real software at Chase Manhattan Bank [»vangR7_1978]

Quote: formally verified Byzantine failure clock synchronization with EHDM; difficult; found many errors, though none serious [»rushJ12_1991]

Quote: a programmer on hearing that a dam had broke spent two days trying to verify his program; it wasn't his dam that failed, but he found many errors [»meerL_1978]

Quote: using Cleanroom techniques, can construct proof arguments for very large software systems

Quote: in Cleanroom, used intensive team reviews to verify two formal grammars of 1500 productions each; no grammar errors found in field testing [»lingRC10_1988]

Quote: using function-theoretic design verification, a team review checked 1200 correctness questions in a few days; astonishing savings during test [»lingRC10_1988]

Quote: survey of cryptology and computational complexity; cryptographic protocols, one-way functions, public-key, interactive proof systems, and zero-knowledge protocols [»rothJ12_2002]

QuoteRef: elspB6_1972 ;;good review (mathematical) of program proof methods

QuoteRef: mannZ5_1978 ;;excellent review of program correctness proving