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.
What one survey section teaches model checking from
A subject the papers are about. The loosest grouping, and the one to reach for last.
A reading path for model checking, following section 6 of `halpern2001unusual` in the order the field built the results. Collects exactly the works that section cites, so the set is a bibliography of one survey section rather than of a subject. That section is titled *Automated verification of semiconductor designs*, which is worth knowing before reading it as a general history.
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)