Possible topics and pointers for survey type term project:

<ul><b>Model Checking Web Services</b>

<ul>Hai Huang, Wei-Tek Tsai, Raymond Paul, and Yinong Chen, <a 
href="http://asusrl.eas.asu.edu/srlab/Publications/OtherPapers/ISORC05-Automated.pdf">Automated 
Model Checking and Testing for Composite Web Services</a>, In Proc. of 
the 8th IEEE International Symposium on Object-Oriented Real-time 
Distributed Computing, 2005, pp. 300-307.</ul><br>

<ul>
Walton, Dr Christopher, 
<a href="http://eprints.aktors.org/295/"> 
Model Checking 
Multi-Agent Web Services. </a>
In Proceedings AAAI Spring Symposium on Semantic Web Services, 
Stanford, California, 2004. </ul><br>

<ul>
Xiang 
Fu, Tevfik Bultan, and Jianwen Su. 
<a href="http://www.cs.ucsb.edu/~bultan/vlab/publications.html">
"Model Checking XML 
Manipulating Software." </a>, 
In  Proceedings of the 2004 ACM/SIGSOFT 
International Symposium on Software Testing and Analysis (ISSTA 
2004), pp. 252-262, Boston, Massachusetts, July 11-14, 2004. </ul> 

</ul><br>


<ul><b>Counter Example Generation</b>

<ul>
G. Pace and N. Halbwachs and P. Raymond. 
<a href="http://www-verimag.imag.fr/~halbwachs/sttt04.html">
Counter-example generation in 
symbolic abstract model-checking. 
</a>
Software Tools for Technology Transfer, 
Vol. 5, No. 2, March 2004. 
</ul><br>

<ul>
<a href="http://ext.math.umass.edu/~avrunin/recent_pubs/">
Heuristic-guided 
counterexample search in FLAVERS. 
</a>
Jianbin Tan, 
George S. 
Avrunin, Lori A. Clarke, Shlomo Zilberstein, and Stefan Leue. 
In Proceedings of the 12th ACM Symposium on the Foundations of Software 
Engineering, pages 201-210, Newport Beach, CA, November 2004. 
 </ul><br>

<ul> 
Sagar Chaki, Alex 
Groce, and Ofer Strichman. 
<a href="http://www-2.cs.cmu.edu/~agroce/pubs.html">
Explaining Abstract 
Counterexamples. 
</a>
In Foundations of Software Engineering (SIGSOFT FSE), 
pages 73--82, Newport Beach, California, October-November 2004. 
</ul><br>

<ul>
Alex Groce. 
<a href="http://www-2.cs.cmu.edu/~agroce/pubs.html">
Error 
Explanation with Distance Metrics. 
</a>
In Tools and 
Algorithms for the Construction and Analysis of Systems (TACAS), pages 
108--122, Barcelona, Spain, March-April 2004. 
</ul><br>

<ul>
Marsha Chechik and Arie Gurfinkel. 
<a href="http://www.cs.toronto.edu/~chechik/pubs">
Proof-Like Counter-Examples
</a>, 
in 
Proceedings of TACAS'03, LNCS 2619, pp. 160-175, April 2003, Springer. 
</ul><br>

<ul>
Corina S. Pasareanu, Matthew B. Dwyer, Willem Visser. 
<a href="http://ase.arc.nasa.gov/people/pcorina/allpapers.html">
Finding Feasible 
Abstract Counter-examples. 
</a>
International Journal on Software Tools for 
Technology Transfer, November 2003, Volume 5, Number 1, 34-48. 
 </ul>
</ul><br>

<ul><b>Modular Verification</b>

<ul>
Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, and Helmut Veith. 
<a href="http://www-2.cs.cmu.edu/~agroce/pubs.html">
Modular Verification of Software Components in C. 
</a> 
IEEE Transactions on 
Software Engineering, Volume 30, Number 6, pages 388--204, June 2004. 
 </ul><br>

<ul>
Dimitra Giannakopoulou, Corina S. Pasareanu, Howard Barringer. 
<a href="http://ase.arc.nasa.gov/people/pcorina/allpapers.html">
Component Verification with Automatically Generated Assumptions.
</a>
 To appear 
in Journal of Automated Software Engineering, Kluwer Academic Publishers. 
</ul><br>

<ul>
Kathi Fisler and Shriram Krishnamurthi.
<a href="http://www.cs.brown.edu/~sk/Publications/Papers/Published/fk-mod-verif-collab/">
Modular Verification of Collaboration-Based Software Designs.
</a>
Joint European Software Engineering Conference and ACM SIGSOFT Symposium 
on the Foundations of Software Engineering, 2001.
</ul><br>

<ul>
C. Flanagan and S. Qadeer. 
<a href="http://research.microsoft.com/~qadeer/">
Thread-modular model checking. 
</a>
Proceedings of 
the SPIN Workshop on Software Verification, 2003.
</ul>

</ul>

<ul><b>Predicate Abstraction</b>

<ul>
Sagar Chaki, Edmund 
Clarke, Alex Groce, and Ofer Strichman. 
<a href="http://www-2.cs.cmu.edu/~agroce/pubs.html">
Predicate 
Abstraction with Minimum Predicates. 
</a>
In Advanced Research Working 
Conference on Correct Hardware Design and Verification Methods (CHARME), 
pages 19--34, L'Aquila, Italy, October 2003. 
</ul><br> 

<ul>
Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. 
<a href="http://www.cs.ucla.edu/~todd/research/pldi01.html">
Automatic Predicate Abstraction of C Programs.
</a>
Proceedings of the Conference on Programming Language Design and 
Implementation (PLDI 2001), Snowbird, Utah, June 20-22, 2001. 
</ul><br>

<ul>
Satyaki Das and David L. Dill. 
<a href="http://chicory.stanford.edu/satyaki/research/PredicateAbstraction.html">
"Counter-Example Based Predicate Discovery 
in Predicate Abstraction", 
</a>
In Proceedings of FMCAD 2002, Portland, Oregon, 
USA, November, 2002. 
 </ul><br>

<ul>
Cormac Flanagan and Shaz Qadeer. 
<a href="http://portal.acm.org/citation.cfm?id=503291">
Predicate abstraction for software 
verification. 
</a>
Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on 
Principles of programming languages.  
</ul>

</ul>