Reading group

Schon gelesen:

• 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

Steht noch an:

• 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

Wird nicht gelesen:

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