Group: requirement specification
Group: testing
Topic: automated tests of specifications and designs
Topic: consistency testing
Topic: embedded systems
Topic: error safe systems
Topic: formal methods and languages
Topic: hardware vs. software
Topic: limitations of formalism
Topic: limitations of system security
Topic: mathematical proof as a social process
Topic: model checker
Topic: problems with logic programming
Topic: program source as truth
Topic: specification is infeasible
 
Summary
Program proofs are notorious for their length, complexity and error proneness. Only highly trained researchers have attempted proofs of any size. There are several weaknesses: (1) Program proving is an isolated phenomenon used as a formal exercise. It is unlike mathematics where proofs are used to simplify and provide foundations for further development. (2) Proofs are only possible if the program is already correct. They will not show where a program is incorrect nor do they indicate incorrect programs. (3) Proofs are dependent upon a correct specification of criterion. A proof only demonstrates a consistent program representation, not a representation which is valid, maintainable, useful, and efficient. (cbb 5/80)
Program proofs ignore the possibility of errors in the program's environment. A proof may be too costly, and it may encourage the removal of useful redundancies. In short, proving a program does not make the program trustworthy. Program proofs remain a useful consistency check for safetycritical programs. (cbb 12/92)
Subtopic: practical formal methods
Quote: use formal methods to verify a design instead of proving correctness; forces engineers to be precise about details; resolves differences of interpretation between implementers and testers [»tretJ9_2001]
 Quote: program proving and automatic derivation of code from formal specifications are not important; e.g., implementation of formal specifications caused few errors [»tretJ9_2001]
 Subtopic: problem of reliability and trustworthiness
Quote: a verified program is provably corrected but not reliable and trustworthy; no information about limits [»demiRA5_1979]
 Quote: nothing can prove the absence of bugs; verification can not prevent failures from unforeseen causes [»abraP12_1986]
 Quote: program verification does not provide reliability, safety, or security; it proves limited design correctness [»dobsJ4_1989]
 Subtopic: proof as consistency checking
Quote: logic is not flexible enough for thinking because consistency is too strong a requirement [»minsM_1981]
 Quote: validation methods are primarily used as bugfinders; formal methods are useful because they find different bugs than traditional methods; a more realistic goal than guaranteeing correctness [»dillDL4_1996]
 Quote: proving a hardware design is just another form of checking; does not catch specification errors and analog behavior [»wilkM10_1990]
 Quote: program verification useful for clarifying specifications and removing design faults; not for guaranteed correctness [»dobsJ4_1989]
 Quote: instead of 'proof of correctness', should use 'proof of relative consistency'
 Quote: consistent, closed, complete methods are limited for elucidating truth [»gammRC10_1974]
 Quote: a program proof is for refutation of certain forms of incorrectness; math proofs demonstrate existence [»dobsJ4_1989]
 Subtopic: problem of specification errors
Quote: uncaught errors in executable specification languages are just as disastrous as in traditional programming [»abboRJ3_1990]
 Quote: neither structured programming nor proofs of correctness attempt to check the specification itself [»bateD_1976]
 Quote: proof may show that a program matches its specifications, but does not tell if the specifications are correct [»gammRC10_1974]
 Quote: a formal specification also requires user feedback from an implementation [»abboRJ3_1990]
 Quote: a program can be wrong only because the customer wanted a different function to be calculated [»scowRS3_1982b]
 Quote: only testing reveals discrepancies between a model and the real situation; also errors in proofs [»parnDL6_1990]
 Subtopic: proof is social
Quote: an important part of 'proof' in mathematics is the social mechanism; does not exist for proving programs [»demiRA_1977]
 Quote: simple, unspecialized theorems become part of mathematics, but program proving produces narrow theorems for a paltry class of structures [»demiRA_1977]
 Quote: a verification of a program must be accepted blindly without the social processes of mathematical proofs [»demiRA5_1979]
 Quote: a verification may not be transferable to any other program; prevents social processes [»demiRA5_1979]
 Quote: the details of the proof of Smallintset are complex and not included with this paper [»hoarCA_1972a]
 Subtopic: engineers do not prove
Quote: there are no proofs that bridges stand, that airplanes fly, or that power systems deliver electricity
 Quote: in a mature engineering discipline, 'reliable' never means 'perfect' [»demiRA_1977]
 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]
 Subtopic: proof not possible
Quote: since a program is a human artifact it will contain imperfections and can never be verified [»demiRA5_1979]
 Quote: a program is the only complete description of the program's behavior [»demiRA5_1979]
 QuoteRef: cbb_1973 ;;11/3/74 one can not prove a space of representation
 Subtopic: problem of exceptions
Quote: analyzing exceptions for correctness is difficult [»cargT11_1994]
 Subtopic: problem of invalid data
Quote: program verification assumes that nonsensical operations do not occur; i.e., data is valid [»stroRE1_1986]
 Subtopic: problem of sideeffects
Quote: languages in which erroneous programs have arbitrary sideeffects are nonsecure because every module must be proven error free before any can be [»stroRE5_1985]
 Subtopic: problem of feature interaction
Quote: feature interaction makes program validation complicated [»wassAI3_1979]
 Subtopic: problem of efficiency
Quote: full formal development with machinechecked proofs is too expensive except for failurecritical applications
 Quote: model checkers find a few difficult errors with simplified code; metalevel compilation works directly with program source and found many errors [»chouA11_2000]
 Quote: reliability is only one of many desired properties; high reliability may cost too much [»gammRC10_1974]
 Quote: the construction of symbolic structures uses resources; can be impossibly long if care is not taken [»demiRA5_1979]
 Quote: proofs with a general purpose theorem prover may almost always be impractically long [»rabiMO8_1974]
 Quote: there are always short true statements concerning the addition of natural numbers whose formal proof is superexponentially long [»rabiMO8_1974]
 Subtopic: problem of finding invariants
Quote: proving program correctness depends on knowing the invariants satisfied by the program; given a complicated program may be difficult to find [»baueFL_1976]
 Quote: it is hard to find 'the' invariant when a program is wrong [»baueFL_1976]
 Quote: Hoare axioms exist for at most 4 of 5 blockstructured features: procedure parameters, recursion, static scope, globals, internal procedures [»clarEM1_1979]
 Subtopic: program verification not done
Quote: program proofs, crossreferences, attribute lists, and dumps were rarely used
 Quote: program verification is a shared joke among programmers; something that must be learned and then ignored
 Subtopic: proof removes redundancies
Quote: if we feel that something is provably right then redundancies are removed [»demiRA5_1979]
 Subtopic: successful proof checking
Quote: certified evaluation via a proof checker for lists of facts, security rules, and derivations; 100 lines of code [»jimT5_2000]
 Quote: verifying a finite state model is much easier that fully understanding a system's behavior; e.g., only four operations on user IDs [»chenH8_2002]

Related Topics
Group: requirement specification (11 topics, 307 quotes)
Group: testing (18 topics, 557 quotes)
Topic: automated tests of specifications and designs (12 items)
Topic: consistency testing (60 items)
Topic: embedded systems (26 items)
Topic: error safe systems (76 items)
Topic: formal methods and languages (53 items)
Topic: hardware vs. software (15 items)
Topic: limitations of formalism (93 items)
Topic: limitations of system security (39 items)
Topic: mathematical proof as a social process (14 items)
Topic: model checker (49 items)
Topic: problems with logic programming (10 items)
Topic: program source as truth (17 items)
Topic: specification is infeasible (46 items)
