Dr. Allen Goldberg

Kestrel Institute
3260 Hillview Avenue
Palo Alto
CA 94304
U.S.A.
tel:(+1) 650-493-6871
fax:(+1) 650-424-1807
e-mail:

Current Activities

See my new paper "A specification of Java Loading and Bytecode Verification", abstract, PDF 154KB

Member of program committee for the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering PASTE'98

Research Interests

  • Transformational development of code from specifications. Formalization of programming knowledge, especially data structure design, software architectures, parallel programming, and high-level program optimization. I have contributed to the development of Specware, Reacto, DTRE, Proteus, and KIDS.
  • Formalization of Java Bytecode verification. In our most current work we are using Specware to formalize the portion of Java bytecode verifier that use data flow analysis to type check java virtual machine code. This work is being carried out as part of the DARPA CPR project.
  • Program analysis. The use of symbolic evaluation and tracatble inference methods to assist in prgram analysis problems such as program testing, slicing, and program understanding.

Selected Publications

  • Qian, X., Goldberg, A. Bounds Analysis by Abstract Interpretation. First Workshop on Automated Analysis of Programs, Paris, France, 1997. (postscript, dvi)

  • A. Goldberg, J. Prins, J. Reif, R. Faith, Z. Li, P. Mills, L. Nyland, D. Palmer, J. Riely, S. Westfold, "The Proteus System for the Development of Parallel Applications", in Prototyping Languages and Prototyping Technology, M. Harrison, ed., (to appear) Springer-Verlag, 1996. (40 pp) abstract, postscript.

  • Goldberg, A., Mills, P., Nyland, L.,Prins, P., Reif, J., Riely, J. Specification and Development of Parallel Algorithms with the Proteus System, DIMACS Workshop on Specification of Parallel Algorithms, G. Blelloch, M. Chandy, and S. Jagannathan,ed. AMS, 1995 , pp 383-399. abstract, postscript.

  • Goldberg, A., R. Furst C. Green, "A Refinement Approach to Visualization, " Kestrel Institute Report, 1995. postscript.

  • Goldberg, A., Wang, T.C., Zimmerman, D.. Applications of Feasible Path Analysis to Program Testing, Proceedings of the International Symposium on Software Testing and Analysis, Seattle, WA, Aug. 1994. postscript.

  • Wang T.C. and Goldberg, KITP-93: An automated Inference System for Program Analysis, Proceedings of 12th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence (ed. A. Bundy), vol. 814, pp. 831-836 (1994). postscript, dvi

  • Qian,X., Goldberg, A. Referntial Opacity in Non-Deterministic Data Refinement, ACM Letters on Programming Languages and Systems no. 1-4 pp 233-41, March 1993. postscript, dvi.

  • Wang, T.C. and Goldberg, A. RVF: An Automated Formal Verification System. Proceedings of the 11 th Conference on Automated Deduction, Lecture Notes in Computer Science (ed. D. Kapur), vol. 607, pp. 735-739 (1992).

  • Wang, T.C. and Goldberg, A. A Mechanical Verifier for Supporting the Design of Reliable Reactive Systems. Appeared in, International Symposium on Software Reliability Engineering, Austin, TX, May 1991. Kestrel Institute Technical Report KES.U.91.6, May 1991.

  • Blaine, L. and Goldberg, A. DTRE -- A Semi-Automatic Transformation System. Appeared in, Constructing Programs from Specifications. B. Möller, Ed., North Holland,.1991 postscript, dvi.

  • Goldberg, A., Reusing Software Developments. Proceedings of the ACM SIGSOFT 4th Symposium on Software Development Environments, December 1990. postscript, dvi (Note figures are omitted)

  • Gilham, L., Goldberg, A. and Wang, T.C., Toward Reliable Reactive Systems, Proceedings of the Fifth International Workshop on Software Specification and Design, Pittsburgh, PA, May, 1989, pp. 68-74.

  • Goldberg, A., Knowledge-Based Programming: A Survey of Program Design and Construction Techniques. IEEE Transactions on Software Engineering, July 1986.

  • Goldberg, A., and Paige, R., Stream Processing. Proceedings of the 1984 Conference on LISP and Functional Programming, Austin, Texas, pp. 53-62.

  • Goldberg, A., Purdom, P. and Brown, C., Average Time Analysis of Simplified Davis-Putnam Procedures. Information Processing Letters, Volume 15, Number 12, 1982.

  • Goldberg, A., Average Case Complexity of the Satisfiability Problem. Proceedings of the Fourth Workshop on Automated Deduction, Austin, Texas, February 1979.