- Shuvendu K. Lahiri, Randal Bryant. "Constructing Quantified Invariants via Predicate Abstraction". A version which contains a bit more proofs but is less compact is called "Predicate Abstraction with Indexed Predicates" (probably unreviewed). Following paper is claimed to be useful for getting the whole picture:

S. K. Lahiri, R. Bryant. "Indexed Predicate Discovery for Unbounded System Verification"

as well as some paper on logic is needed. - Predicate Abstraction for Software Verification. Cormac Flanagan and Shaz Qadeer. In POPL 02, pages 191-202. ACM, January 2002.
- Patrick Cousot, "Partial completeness of Abstract Fixpoint Checking", B.Y. Choueiry and T. Walsh (Eds.): SARA 2000, LNAI 1864, pp. 1-25, 2000

- From Dexter Kozen, "Lower bounds for natural proof systems": a proof that nonemptiness of intersection of regular automata is PSPACE-complete.

Question: is any average-case analysis known? - C. Flanagan, S.N. Freund, and S. Qadeer. "Exploiting purity for atomicity." Proceedings of the International Symposium on Software Testing and Analysis, 2004 (Distinguished Paper Award).
- Patrice Godefroid, Pierre Wolper. "A Partial Approach to model checking." Additional literature: a thesis of P. Godefroid "Partial-Order Methods for the Verification of Concurrent Systems An Approach to the State-Explosion Problem"
- Peter Habermehl, Tomas Vojnar. "Regular model checking using inference of regular languages". (or some other paper on regular model checking)
- Slicing
- Alternating finite automata
- Automata-theoretic aspects of formal power series
- W. Thomas. Automata on infinite objects.
- TATA. Hubert Comon, Max Dauchet, Remi Gilleron, Florent Jacquemard, Denis Lugiez, Sophie Tison, Marc Tommasi. http://www.grappa.univ-lille3.fr/tata/
- Deciding assertions in Programs with references. Shaz Qadeer; Sriram K. Rajamani
- Nils Klarund, Anders Møller, Michael I. Schwartzbach. MONA implementation secrets. CIAA'00
- Giacobazzi, Ranzato, Scozzari. Making abstract interpretations complete. JACM, 2000
- Kenneth McMillan. Lazy abstractions with interpolants. CAV'06
- Bouajjani, Bozga, Habermehl, Iosif, Moro, Vojnar. Programs with lists are counter automata. CAV'06
- Rajeev Alur, Swarat Chaudhuri, P. Madhusudan. Language of nested trees. CAV'06
- Chin Soon Lee. Ranking functions for size-change termination. submitted to TOPLAS.
- Bounded Algol-like languages. Seymour Ginsburg and Edwin H. Spanier

+

Semigroups, Presburger Formulas, and Languages. Seymour Ginsburg and Edwin H. Spanier - Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation. P. Cousot, R. Cousot
- Environment Abstraction for Parameterized Verification. E. Clarke, M. Talupur, H. Veith
- Polymorphic Predicate Abstraction. T. Ball, T. Millstein, S. Rajamani
- Software Model-Checking: The VeriSoft Approach. P. Godefroid + his diss as auxiliary material
- A unified approach for studying the properties of transition systems. Joseph Sifakis
- Automated, Compositional and Iterative Deadlock Detection. S. Chaki, E. Clarke, J. Ouaknine, N. Sharygina
- The JAVA memory model. J. Mason, W. Pugh, S. V. Adve
- An efficient algorithm to compute the synchronized product. Denis Zampunieris, Baudouin Le Charlier
- Invariance Proof Methods And Analysis Techniques For Parallel Programs. P. Cousot, R. Cousot, 1984
- Comparing Completeness Properties Of Static Analyses And Their Logics. Dave Schmidt, Technical Report, 2006.
- Linear-time temporal logic and Buchi automata. Madhavan Mukund
- Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm: Solving Shape-Analysis Problems in Languages with Destructive Updating. POPL 1996: 16-31
- Static Program Analysis via 3-valued logic, CAV'04 invited talk
- Parametric Shape Analysis via a 3-valued logic, TOPLAS'02 (has all details)
- Points-to Analysis in Almost Linear Time, by Bjarne Steensgard, POPL 1996.
- Extended Static Checking for Java. Cormac Flanagan, K. Rustan M. Leino, Mark Lilibridge, Greg Nelson, James B. Saxe, Raymie Stata
- Moshe Y. Vardi. Verification of Concurrent Programs: The Automata-Theoretic Framework
- Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Progress. Draft, 1996

- Rajeev Alur, P. Madhusudan. Visibly pushdown languages. STOC, Symp. on Theory of Computing, Chicago, 2004.