This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
State space, not proof
A subject the papers are about. The loosest grouping, and the one to reach for last.
Verification by searching a program's states rather than deriving its properties. Collects the model-checking line from temporal logic through the algorithms and the tools that implement them. Membership requires the method to be exhaustive search over states; a deductive proof of the same property belongs in the program-logic sets.
7 references
On the unusual effectiveness of logic in computer science
Joseph Y. Halpern and others (2001) · Bulletin of Symbolic Logic
The model checker SPIN
G. J. Holzmann (1997) · IEEE Transactions on Software Engineering · Institute of Electrical and Electronics Engineers (IEEE)
Reasoning about Infinite Computations
Moshe Y. Vardi and others (1994) · Information and Computation · Elsevier BV
An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)
Moshe Y. Vardi and others (1986) · Proceedings of the First Annual Symposium on Logic in Computer Science
Specification and verification of concurrent systems in CESAR
J. P. Queille and others (1982) · 5th International Symposium on Programming · Springer
Design and synthesis of synchronization skeletons using branching time temporal logic
Edmund M. Clarke and others (1981) · Logic of Programs · Springer
The temporal logic of programs
Amir Pnueli (1977) · 18th Annual Symposium on Foundations of Computer Science (sfcs 1977)