These sources concern proving that programs do what they claim. Many are course notes and reference articles. This page lists 18 sources, oldest first where dated.
A discipline of programming
This is a catalog record, not the book. It gives title, author, publisher, date and scan details. The book text is not on the page.
On the Refinement Calculus
The monograph reprints papers by Morgan, Robinson and Gardiner from 1987 and 1988. It covers specification statements, procedures, data refinement and a table of refinement laws. The evidence is definitions, proved laws and worked derivations.
Refinement Calculus Tutorial
The page introduces refinement, the notation for it, and a list of four worked derivations. It links to notation pages and a reference list. The page itself gives definitions and one specification example.
The Halting Problem is a terrible example of NP-Harder
The post is a short argument about how to teach complexity classes. It proposes a grid-movement puzzle as a clearer example far harder than NP. It gives explanation and one comment exchange, not formal proofs.
What can you confidently guarantee about your software?
The thread discusses an ACM Queue article on formal verification and AI. Its commenters mostly argue about e-commerce apps, specs, property-based testing and the cost of proofs. The evidence is opinion and personal experience, with a few links to papers and tools.
Software assurance - Wikipedia
This encyclopedia article defines software assurance and lists its activities, techniques and tools. It then gathers definitions from US agencies and standards bodies. The article is a broad overview. It is written in general terms and cites standards and papers.
Satisfiability modulo theories - Wikipedia
This encyclopedia article defines the SMT problem and the tools that solve it. It explains the eager and lazy solver designs. It includes a large table comparing named solvers. It then lists uses in verification, testing and synthesis.
Tony Hoare - Wikipedia
This encyclopedia biography covers the life, career, awards and writings of Sir Tony Hoare. It quotes two of Hoare's own reflections. One covers the null reference, the other formal methods. The page includes a long list of honours and books. Its evidence is citations to obituaries, interviews and papers.
Denotational semantics - Wikipedia
This encyclopedia article defines denotational semantics and traces its history. It works one example, the factorial function, through successive approximations. It then surveys state, concurrency, data types and how denotations relate to implementations. It is a summary of the field with a long list of references.
AeneasVerif/aeneas: A verification toolchain for Rust programs
This README describes Aeneas, which turns Rust code into pure functional code for proof tools. It covers install steps, usage, backends and current limits. It points to two published papers on the method. The evidence is the project's own description and a test folder.
AeneasVerif/charon: Analyze Rust crates without touching compiler internals
This README describes Charon, a tool that extracts a Rust crate into a JSON file. It explains usage, purpose, limits and build steps. It says plainly that the software is beta. The evidence is the project's own description.
Lecture Notes: Hoare Logic
The notes are Lecture 3 of a course on analysis of software artifacts. They define preconditions, postconditions and Hoare triples. They end with a full proof of a small loop program, step by step.
A Whirlwind Tour - SpecForge User Guide
This is a short chapter from the SpecForge user guide. It shows Lilo, a language for temporal specifications of hybrid systems. It walks through a temperature sensor example and the tool's analyses. The evidence is the example itself.
GUI Ripping: Reverse Engineering of Graphical User Interfaces for Testing
The paper proposes GUI ripping, which builds a test model from a running interface. It describes the algorithm and two implementations, for Windows and for Java Swing. Evidence is timing tables on seven applications and one testing run.
Computation as a Universal and Fundamental Concept
This is a short course description on the Ergo site. It summarises Tim Roughgarden's lectures on computability, fast algorithms and P versus NP. The page lists five lesson titles and an instructor biography. The lectures themselves are not part of the page text.
Basics: Functional Programming in Rocq
The chapter is the first technical chapter of Logical Foundations, Volume 1 of Software Foundations. It mixes prose, Rocq code and graded exercises. It introduces data types, functions, simple proofs and the tactics needed for them.
Hoare: Hoare Logic, Part I
The chapter builds Hoare logic on the Imp language defined in Volume 1. It states a proof rule for each command and proves each rule in Rocq. Exercises extend the logic with new commands.
Hoare2: Hoare Logic, Part II
The chapter continues the Hoare logic chapter. It first teaches decorated programs informally. It then formalizes them in Rocq with an automatic generator of proof obligations. A long section on finding loop invariants uses small example loops.
Glossary
- Access-restricted
- The page's own label for the item; it does not explain the term.
- Assertion
- A logical statement about the values of program variables.
- Borrow checker
- The Rust compiler part that enforces ownership rules.
- Compositionality
- The meaning of a whole is built from the meanings of its parts.
- Constructor
- A named building block used to make values of a data type.
- Crate
- A unit of Rust code, similar to a package or library.
- CRUD app
- An app that mostly creates, reads, updates and deletes records in a database.
- CSP
- Communicating sequential processes, a formal language for describing concurrent programs.
- Data refinement
- Replacing abstract variables in a program with more concrete ones.
- Decidable
- Solvable by an algorithm that always finishes.
- Decorated program
- A program with logical assertions written between its commands.
- Denotation
- The mathematical object that stands for the meaning of a piece of a program.
- Domain
- A mathematical set with an ordering, used to model program meanings.
- DPLL(T)
- A design that couples a SAT search with a solver for one theory.
- Event-flow graph
- A graph showing which interface actions can follow which.
- Extraction
- Turning a Rocq definition into a program in another language.
- Falsification
- A search for an input that makes a system break its spec.
- Fixed point
- A value that a function maps to itself.
- Formal methods
- Mathematical techniques for specifying and verifying software.
- Formal verification
- Proving with mathematics that a program meets a precise statement of what it should do.
- Full abstraction
- Programs that behave the same in every context have equal denotations.
- Fuzz testing
- Feeding random or malformed input to a program to find failures.
- Fuzzing
- Feeding a program random or odd inputs to provoke failures.
- Gallina
- The functional programming language built into Rocq.
- GUI
- Graphical user interface, the windows, buttons and menus a person clicks.
- Halting problem
- The question of whether a program will eventually stop, which no algorithm can always answer.
- Hoare logic
- A formal system for proving that a program meets its specification.
- Hoare triple
- A claim that a command takes states meeting a precondition to states meeting a postcondition.
- Hybrid system
- A system that mixes continuous physical signals with discrete software logic.
- Imp
- A small imperative language used in the course to study programs mathematically.
- Internet Archive
- A nonprofit digital library that hosts scans of books and other media.
- Lambda calculus
- A minimal mathematical language of functions.
- Lint
- An automatic check for suspicious code style.
- LLBC
- The intermediate file format that Charon produces.
- Loop invariant
- A statement that is true before and after every pass of a loop.
- MIR
- Rust's mid-level internal code form used by the compiler.
- Miracle
- A statement that can never be run but eases the algebra of a derivation.
- Modal window
- A window that must be closed before the user can do anything else.
- Model checking
- Exhaustively checking every state of a small model of a system against stated rules.
- Monitoring
- Checking recorded behaviour against a spec after the fact.
- NP
- Decision problems where a yes answer can be checked quickly given a proof.
- NP-complete
- Among the hardest problems in NP, so a fast solution to one would solve all.
- NP-hard
- At least as hard as the hardest problems whose answers can be checked quickly.
- Null reference
- A pointer value meaning no object, which can cause crashes if used.
- Operational semantics
- A way of giving meaning by describing how a program runs step by step.
- P versus NP
- The open question of whether every quickly checkable problem is also quickly solvable.
- Partial correctness
- Correctness that holds only if the program terminates.
- Pattern matching
- Choosing what to compute by the shape of a value.
- PCF
- A small, purely sequential functional language used in semantics research.
- Polynomial time
- Running time that grows as a fixed power of the input size.
- Postcondition
- A condition the code guarantees once it finishes.
- Precondition
- A condition the caller must make true before running the code.
- Proof assistant
- Software that checks mathematical proofs written by people.
- Property-based testing
- Testing a program with many generated inputs to check that a stated rule always holds.
- Quicksort
- A fast sorting method that splits a list around a pivot value.
- Refinement calculus
- A set of rules for turning an abstract specification into a program step by step.
- Regression testing
- Re-running tests after changes to check nothing broke.
- Rocq
- A proof assistant, a program that checks mathematical proofs and runs a small functional language.
- Rustc
- The standard Rust compiler.
- SAT
- The problem of finding true or false values that make a logic formula true.
- Separation logic
- A logic for reasoning about programs that use memory.
- Signal
- A value that changes over time, such as a sensor reading.
- SMT solver
- A program that decides whether a formula can be satisfied under given theories.
- Software assurance
- Confidence that software works as intended and is free from vulnerabilities.
- Spec
- A written statement of what a program is supposed to do.
- Specification statement
- A program fragment that says what must be achieved, not how.
- Static analysis
- Checking code for defects without running it.
- Stepwise refinement
- Building a program by repeatedly replacing abstract parts with more concrete ones.
- Symbolic execution
- Running a program on symbols to find the inputs that reach each path.
- Syntax directed
- Organized so that the steps of a proof follow the shape of the program text.
- Tactic
- A command that guides Rocq through a step of a proof.
- Temporal specification
- A rule about how a system's behaviour should unfold over time.
- Test oracle
- Expected output used to decide whether a test passed.
- Theory
- A set of rules about a kind of object, such as integer arithmetic.
- Threat modeling
- Listing the ways a system could be attacked and how to reduce them.
- Trait
- A Rust feature that describes shared behaviour across types.
- Transitive
- If A leads to B and B leads to C, then A leads to C.
- Traveling Salesman Problem
- Finding the shortest tour that visits every city once.
- Undecidable
- No algorithm can answer the question correctly in every case.
- Variant function
- A whole-number measure that shrinks each pass, which shows the loop must end.
- Verification condition
- A logical fact that must hold for a decorated program to count as a proof.
- Weakest precondition
- The most general starting condition that guarantees a given result.
- Widget
- A single interface element such as a button or text box.
- Witness
- A proof of a yes answer that can be checked.
- Z and VDM
- Two notations for writing formal specifications of software.