CS745 Potential Papers for Presentation

Model Checking

• (Ali R.) Gerard Holzmann,The Spin Model Checker, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295.
• (Ruth) Paul Gastin and Pierre Moro, Minimal Counterexample Generation for SPIN, in Lecture Notes in Computer Science, LNCS 4595, August 2007, pp. 24-38.
  
• (Bryan) Klaus Havelund and Tom Pressburger. Model Checking Java Programs Using Java PathFinder International Journal on Software Tools for Technology Transfer (STTT). Volume 2 Number 4. April 2000.
• (Mazen) Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in Propery Specification for Finite-State Verification. In Proceedings of the 21st International Conference on Software Engineering, May 1999
• Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue, Protocol Verification with Heuristic Search, Proc. AAAI Spring Symposium, AAAI, Stanford, March 2001
• (Colleen) Jamieson M. Cobleigh, Lori A. Clarke, and Leon J. Osterweil, The Right Algorithm at the Right Time: Comparing Data Flow Analysis Algorithms for Finite State Verification. In Proceedings of the International Conference on Software Engineering, 2001.
• Robby, Matthew B. Dwyer, John Hatcliff, Bogor: an extensible and highly modular software model checking framework, In Proceedings of the 9th European Software Engineering Conference held jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2003.
• Thomas Ball and Sriram K. Rajamani, Automatically Validating Temporal Safety Properties of Interfaces International Workshop on SPIN Model Checking, 2001.
• (Mina) Felix Sheng-Ho Chang and Daniel Jackson, Symbolic Model Checking of Declarative Relational Models, In Proceedings of the 28th International Conference on Software Engineering (ICSE), 2006.
• (Ramanan) Baoqiu Cui, Yifei Dong, Xiaoqun Du, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Abhik Roychoudhury, Scott A. Smolka, David S. Warren, Logic programming and model checking, In Proceedings of PLILP/ALP, LNCS 1490.
• (Tariq) Yuan Yu, Panagiotis Manolios, Leslie Lamport, Model Checking TLA+ Specifications. In Proceedings of CHARME 1999.
• For additional papers on software model checking, check out
  
• the SPIN workshop
• the Software Model Checking workshop that is affiliated with the Computer-Aided Verification (CAV) conference
• ISSTA proceedings

Model Finding

• Marcelo F. Frias, Carlos G. Lopez Pombo, Juan P. Galeotti, Nazareno M. Aguirre, Efficient Analysis of DynAlloy Specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), December 2007.
• Emina Torlak and Daniel Jackson, Kodkod: A Relational Model Finder, In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2007

Abstraction

• (Hang) Patrice Godefroid, Pierre Wolper, A Partial Approach to Model Checking, Information and Computation, 1994.
• (Jiewen) Satyaki Das, David L. Dill, Seungjoon Park, Experience with Predicate Abstraction CAV 1999.
• (Ali N.) Bharadwaj, Ramesh and Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction Automated Software Engineering, Vol 6, No. 1, pp. 37-68, January 1999, Kluwer Academic Publishers
• (Ana) William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, and Jon D. Reese Model checking large software specifications, IEEE Transactions on Software Engineering, 1998.
• Thomas Ball and Sriram K. Rajamani Automatically Validating Temporal Safety Properties of Interfaces SPIN 2001.
• Matthew Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, Hongjun Zheng Tool-supported Program Abstraction for Finite-state Verification in Proceedings of the 23rd International Conference on Software Engineering, May, 2001.
• (Zihon) Jerry R. Burch and David L. Dill, Automatic Verification of Pipelined Microprocessor Control, in Proceedings of Computer Aided Verification, LNCS 818, 1994.
  

Compositional Reasoning

• Sergey Berezin, Sergio Campos, Edmund M. Clarke, Compositional reasoning in model checking, In Proceedings of International Symposium on Compositionality (COMPOS), 1998.
• (Eugene) Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson, Modular Verification of Code with SAT, In Proceedings of International Symposium on Software Testing and Analysis, 2006.
• Kedar Namjoshi and Richard Trefler On The Completeness of Compositional Reasoning CAV 2000.
• K.L. McMillan, Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking, Computer Aided Verification (CAV), 1998.
• (Tejas) Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, and Thomas F. Melham Practical Formal Verification in Microprocessor Design, IEEE Design and Test, 2001.

Other Verification Techniques

• Carl-Johan H. Seger and Randal E. Bryant,  Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories, in Formal Methods in System Desig, Vol. 6, No. 2, pp. 147-189, March 1995.  Kluwer Academic Publishers.
• (Cameron) Matthew W. Moskewicz, Conor F. Madigan, Chaff: Engineering an Efficient SAT Solver, In Proceedings of Design Automation Conference, 2001.