Topic: constructing proof and program together
Topic: Goldstine and von Neumann consistency proof
Topic: safety, liveness, and system properties
Topic: predicate transforms
Topic: program proof via assertions
Topic: program proving is infeasible
Topic: proofcarrying code
Topic: proving concurrent programs
Topic: theorem proving systems
Topic: transformation of programs
Group: formalism
Group: requirement specification
Group: security
Group: testing
Group: type checking
Topic: abstract data type
Topic: automated tests of specifications and designs
Topic: Cleanroom software development
Topic: consistency testing
Topic: error safe systems
Topic: exceptions from invalid input
Topic: flavor analysis and typestates for supplementary type checking
Topic: formal methods and languages
Topic: logic
Topic: mathematical proof as a social process
Topic: mobile code
Topic: model checker
Topic: programming as mathematics
Topic: programming without errors
Topic: safety critical systems
Topic: semantics by an abstract machine
Topic: typesafe and secure languages
 
Summary
A dream of computer scientists is to manipulate mathematical program representations just like hardware engineers manipulate mathematical representations of analog circuits and structural materials. In particular they want to prove or demonstrate certain program properties. Proofs are possible if the programming language has a formal semantics. This is the case with reduction languages and Lisp. In critical software for banking, control, and military applications limited proofs are necessary. All proofs should be usable and derivable by others. They should not depend on a particular implementation or data representation, but test data can give hints for proof derivation. Proofs would be a measure of program complexity; simple proofs would indicate a simple program. The proof technique would become a program construction method, i.e., a valid proof would be convertible to a valid program. But proofs and programs may be contradictory. For instance the parallel with engineering mathematics is invalidated by the abstract nature of programs. Unlike engineering materials, programs are never real objects ready to be modeled. (cbb 5/80)
Subtopic: importance of proof
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
 Subtopic: specification vs. representation
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: spectypes 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 spectypes 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]
 Subtopic: correctness vs. safety
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 safetycritical 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
 Subtopic: model checking
Quote: rigorous, detailed, readable specification from realworld 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)
 Subtopic: function composition
Quote: sequential execution is function composition; a neat, simple model with deterministic results [»leeEA5_2006]
 Subtopic: hierarchical proof
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]
 Subtopic: type system
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 cachecoherence protocol with four processors, one cache line, and two data values [»dillDL4_1996]
 Subtopic: test cases
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]
 Subtopic: methods of proof
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 APLlike 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 sideeffects by erroneous programs to inappropriate results of the correct type; by typestate checking [»stroRE5_1985]
 Subtopic: security proof
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]
 Subtopic: examples of verified programs
Quote: programmers and implementers use the formal specification of Modula3 threads [»birrAD_1991a]
 Quote: an untrained user found an error in the formal specification of Modula3 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 functiontheoretic design verification, a team review checked 1200 correctness questions in a few days; astonishing savings during test [»lingRC10_1988]
 Subtopic: reviews
Quote: survey of cryptology and computational complexity; cryptographic protocols, oneway functions, publickey, interactive proof systems, and zeroknowledge protocols [»rothJ12_2002]
 QuoteRef: elspB6_1972 ;;good review (mathematical) of program proof methods
 QuoteRef: mannZ5_1978 ;;excellent review of program correctness proving

Group: program proving
Topic: constructing proof and program together (22 items)
Topic: Goldstine and von Neumann consistency proof (6 items)
Topic: safety, liveness, and system properties (22 items)
Topic: predicate transforms (7 items)
Topic: program proof via assertions (61 items)
Topic: program proving is infeasible (47 items)
Topic: proofcarrying code (7 items)
Topic: proving concurrent programs (37 items)
Topic: theorem proving systems (20 items)
Topic: transformation of programs (27 items)
Related Topics
Group: formalism (9 topics, 478 quotes)
Group: requirement specification (11 topics, 307 quotes)
Group: security (23 topics, 874 quotes)
Group: testing (18 topics, 557 quotes)
Group: type checking (12 topics, 392 quotes)
Topic: abstract data type (64 items)
Topic: automated tests of specifications and designs (12 items)
Topic: Cleanroom software development (38 items)
Topic: consistency testing (60 items)
Topic: error safe systems (76 items)
Topic: exceptions from invalid input (4 items)
Topic: flavor analysis and typestates for supplementary type checking (68 items)
Topic: formal methods and languages (53 items)
Topic: logic (84 items)
Topic: mathematical proof as a social process (14 items)
Topic: mobile code (14 items)
Topic: model checker (49 items)
Topic: programming as mathematics (27 items)
Topic: programming without errors (28 items)
Topic: safety critical systems (32 items)
Topic: semantics by an abstract machine (38 items)
Topic: typesafe and secure languages (43 items)
