Group: program proving

topics > computer science > Group: programming

constructing proof and program together
Goldstine and von Neumann consistency proof
safety, liveness, and system properties
predicate transforms
program proof via assertions
program proving is infeasible
proof-carrying code
proving concurrent programs
theorem proving systems
transformation of programs
requirement specification
type checking

abstract data type
automated tests of specifications and designs
Cleanroom software development
consistency testing
error safe systems
exceptions from invalid input
flavor analysis and typestates for supplementary type checking
formal methods and languages
mathematical proof as a social process
mobile code
model checker
programming as mathematics
programming without errors
safety critical systems
semantics by an abstract machine
type-safe and secure languages


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 up

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 up

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]

Subtopic: correctness vs. safety up

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

Subtopic: model checking up

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)

Subtopic: function composition up

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

Subtopic: hierarchical proof up

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 up

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]

Subtopic: test cases up

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 up

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]

Subtopic: security proof up

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 up

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]

Subtopic: reviews up

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

Group: program proving up

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: proof-carrying code (7 items)
Topic: proving concurrent programs (37 items)
Topic: theorem proving systems (20 items)
Topic: transformation of programs
(27 items)

Related Topics up

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: type-safe and secure languages
(43 items)

Updated barberCB 12/05
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.