Design Code Analysis Publications

1999

Darrell Kindred and Jeannette M. Wing
"Theory Generation for Security Protocols"
ACM TOPLAS, July 1999.

Robert O'Callahan
"Optimizing a Solver of Polymorphism Constraints: SEMI"
Technical report CMU-CS-99-13.

Robert O'Callahan
"The Design of Program Analysis Services"
Technical report CMU-CS-99-135.

C.A. Damon, R. Melton, R.J. Allen, E. Bigelow, J.M. Ivers, and D. Garlan
"Formalizing a Specification for Analysis: The HLA Ownership Properties"
Technical report CMU-CS-99-126.

Robert O'Callahan
"A Simple, Comprehensive Type System for Java Bytecode Subroutines"
Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages, January 20-22, 1999.

1998

Mandana Vaziri, Nancy Lynch, and Jeannette M. Wing
"Proving Correctness of a Controller Algorithmn for the RAID Level 5 System
Proceedings of the International Symposium on Fault-Tolerant Computing, 1998.
Also technical report CMU-CS-98-117.

Daniel Jackson, Yuchung Ng, and Jeannette Wing
"A Nitpick Analysis of Mobile IPv6"
Formal Aspects of Computing, September 1997. Also technical report CMU-CS-98-113.

1997

Y. Ng
"A Nitpick Specification of IPv6"
B.S.in Computer Science 1997.

Robert O'Callahan and Daniel Jackson
"Lackwit: A Program Understanding Tool Based on Type Inference"
Proceedings of the 19th International Conference on Software Engineering (ICSE '97), pp. 338-348.

Jeannette Wing and M. Vaziri-Farahani
"A Case Study in Model Checking Software Systems"
Science of Computer Programming, Vol. 28, 1997, pp. 273-299.

1996

Craig Damon, Daniel Jackson, and Somesh Jha
"Checking Relational Specifications with Binary Decision Diagrams"
Proceedings of the Fourth ACM SIGSOFT Conference on Foundations of Software Engineering, San Francisco, CA, October 1996, pp.70-80.

R. O'Callahan and D. Jackson
"Practical Program Understanding with Type Inference"
Technical report CMU-CS-96-130.

Daniel Jackson, Craig Damon, and Somesh Jha
"Faster Checking of Software Specifications"
Proceedings of the ACM Conference on Principles of Programming Languages, St. Petersburg Beach, FL, January 1996, pp. 79-90.

Daniel Jackson, Somesh Jha, and Craig Damon
"Isomorph-free Model Enumeration: A New Method for Checking Relational Specifications"
ACM Transactions on Programming Languages and Systems.

C.A. Damon and D. Jackson
"Efficient Search as a Means of Executing Specifications"
Proceedings of the Conference on Tools for Construction and Analysis of Software, January 1996.

D. Jackson and C.A. Damon
"Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector"
Proceedings of the International Symposium on Software Testing and Analysis, January 1996.

D. Jackson, S. Jha, and C.A. Damon
"Faster Checking of Software Specifications by Eliminating Isomorphs"
Proceedings of the Conference on the Principles of Programming Languages, January 1996.

D. Jackson
"Nitpick: A Checkable Specification Language"
Proceedings of the Workshop on Formal Methods in Software Practice, January 1996.

D. Jackson and M. Jackson
"Problem Decomposition for Reuse"
Software Engineering Journal, January 1996.

1995

D. Jackson and C.A. Damon
"Semi-executable Specifications"
Technical report CMU-CS-95-216.

J.M. Wing and M. Vaziri-Farahani
"Model Checking Software Systems: A Case Study" Proceedings of the SIGSOFT Foundations of Software Engineering, October 1995, Also technical report CMU-CS-95-128.

J.M. Wing and M. Vaziri-Farahani
"A Case Study in Model Checking Software Systems"
Science of Programming, September 1995.

R. O'Callahan and D. Jackson
"Detecting Shared Representations Using Type Inference"
Technical report CMU-CS-95-202.

D. Jackson and S. Jha
"Faster Checking of Software Specifications by Eliminating Isomorphs"
Proceedings of the Conference on Principles of Programming Languages, July 1995.

D. Jackson
"Aspect: Detecting Bugs with Abstract Dependences"
ACM Transactions on Software Engineering and Methodology, April 1995.

J.G. Rivera and A.A. Danylyszyn
"Formalizing the Uni-processor Simplex Architecture"
Technical report CMU-CS-95-224.

1994

D. Jackson and E. Rollins
"A New Model of Program Dependences for Reverse Engineering"
Proceedings of the ACM Symposium on Foundations of Software Engineering, December 1994.

D. Jackson and E. Rollins
"Abstraction Mechanisms for Pictorial Slicing"
Proceedings of the Third Workshop on Program Comprehension, November 1994.

D. Jackson
"Abstract Model Checking of Infinite Specifications"
Proceedings of Formal Methods Europe, October 1994.

D. Jackson and D. Ladd
"Semantic Diff: A Tool for Summarizing the Effects of Modifications"
Proceedings of the Conference on Software Maintenance, September 1994.

R. Harper, P. Lee, F. Pfenning, and E. Rollins
"A Compilation Manager for SML/NJ"
Proceedings of the ACM WorkShop Standard ML, June 1994.

D. Jackson
"Exploiting Symmetry in the Model Checking of Relational Specifications"
Technical report CMU-CS-TR-94-219.

See also: Chopshop and Nitpick's home pages.

Brought to you by the Composable Software Systems Research Group of the School of Computer Science at Carnegie Mellon University.

Email: Maintainer

Modified: 25-Jul-2002