Allen Goldberg

Contact Information

Professional Interests

I'm interested in practical, commercializable tools to improve software and system construction. I have played key technical and managerial roles in such projects in both acdemic and commercial settings.

Currently, as chief architect of the Fusion project, an incubator with in Cadence Design Systems,

Fusion is an environment for model-based development of embedded systems:

• Common semantic representation of multiple modeling frameworks
• Integrated execution of imported SysML and Simulink models
• Cycle-accurate execution of SysML models
• SystemC code generator
• Checking of execution against SysML sequence diagrams
• System analysis framework enabling design choice representation, quantitative, constraint-based comparative analysis of design choices with design quantities informed by dynamic analysis
• Server/client architecture for collaborative systems engineering enables sharing of models, analysis results, constraints and design structures.

I have developed a  runtime verification tool called Eagle. Runtime Verification is a hybrid formal methods and testing technology in which programs are monitored for conformance to properties often stated in temporal logic. A natural extension of runtime verification is the detection and automated recovery of program faults. I am also interested in verification of autonomy software, such a planning and scheduling software used in NASA missions.

Read here for more details regarding my research interests.

A short white paper on software fault protection can be found here.

Current Position

Professional Activities

Organizer: ICAPS 2005 Workshop on Verification and Validation of Planning and Scheduling

Program Committee Member:  ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, International Conference on Theorem Provers and Circuit Design, International Conference on Compiler Construction, Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems, part of the 2005 International Conference on Automated Planning and Scheduling.

Reviewer:  NSF, IEEE Transactions on Software Engineering, Computer Surveys,  ACM Transactions on Programming Languages and Systems, and IEEE Software.

Tutorials: Knowledge-Based Software Development, for IEEE tutorial program; Formal Software Development, PUCI, Rio De Janeiro, and IBM Brazil, Formal Software Development, University of Linköping, Linköping, Sweden

Affiliations: ACM, IEEE,  IFIP Working Group 2.1

Publications

Anton, J., E. Bush, A. Goldberg, K. Havelund, D. Smith, A. Venet, “Towards the Industrial Scale Development of Custom Static Analyzers,” NIST Static Analysis Summit, June, 2006. pdf

Artho, C.,  D. Drusinsky, H. Barringer, A. Goldberg, K. Havelund, S. Khurshid, M. Lowry, C. Pasareanu, G. Rosu, K. Sen, W. Visser, R. Washington, “Combining test case generation and runtime verification,” Theoretical Computer Science 336 (2005), pp. 209-234.

K. Havelund and A. Goldberg, “Verify Your Runs”, Proceedings of the Grand Verification Challenge Workshop, Verified Software: Theories, Tools, Experiments” Zurich, October 2005 (invited paper). pdf

Goldberg, A  and K. Havelund Automated Runtime Verification with Eagle”, paper and invited talk, Verification and Validation of Enterprise Information Systems (VVEIS ’05), May, 2005.   pdf

Goldberg, A., K. Havelund, C. McGann, “Runtime Verification for Autonomous Spacecraft Software”, 2005 IEEE Aerospace Conference. pdf

Barringer, H., A. Goldberg, K. Havelund and K. Sen , “Rule-Based Runtime Verification”, VMCAI'04, Fifth International Conference on Verification, Model Checking and Abstract Interpretation, January 11-13, Venice, Italy, 2004. pdf

Goldberg, A.,  and K. Havelund, “ Instrumentation of Java Bytecode for Runtime Analysis, FTfJP'03, Fifth ECOOP Workshop on Formal Techniques for Java-like Programs, Darmstadt, Germany, July 21, 2003. pdf

Brat, G., D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, W. Visser, R. Washington, “Experimental Evaluation of Verification and Validation Tools on Martian Rover Software’, Journal version of CMU/SEI paper, to appear in Formal Methods in System Design. pdf

Artho, C.,  D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu and W. Visser, “Experiments with Test Case Generation and Runtime Analysis,” ASM 2003, 10th International Workshop on Abstract State Machines, Taormina, Italy, March 3-7, 2003. pdf

Havelund, K., A. Goldberg, R. Filman, G. Rosu, “Program Instrumentation and Trace Analysis,” Invited paper, Monterey Workshop 2002, Radical Innovations of Software and Systems Engineering in the Future, Venice, Italy, October 7-11, 2002  Full version to appear in LNCS. pdf 

Coglio, A., and Goldberg, A., “Type Safety in the JVM: Some Problems in Java 2  (SDK 1.2) and Proposed Solutions,”  Concurrency and Computation: Practice and Experience , 13(13):1153-1171, November 2001.  pdf
Short version appeared in 2nd ECOOP Workshop on Formal Techniques for Java Programs, June 2000. pdf

Qian, Z., Goldberg, A., and Coglio, C., “A Formal Specification of Java Class Loading,” in Proceedings of the 15^th ACM Conference on Object-Oriented Programming (OOPSLA’ 00), pp. 325—336, Oct. 2000. pdf
Long version appeared as Kestrel Institute Technical Report KES.U.00.10, April 2000, revised July 2000.  pdf 

Martin, B. White, P. Goldberg, A., Taylor, F.,  “Formal Construction of the Mathematically Analyzed Separation Kernel” ACM Sigart Conference on Automated Software Engineering (ASE 2000), Grenoble, France, Oct. 2000. pdf

Coglio, A., and Goldberg, A., “Type Safety in the JVM: Some Problems in JDK 1.2.1 and Proposed Solutions,” Proc. 2^nd ECOOP Workshop on Formal Techniques for Java Programs, Oct.  2000. (conference version). pdf

Nyland, L.,  Prins, J.,  Goldberg, A., and Mills, P., “ A Design Methodology for Data-Parallel Applications,”  IEEE Transactions of Software Engineering, Special Issue on Architecture-Independent Languages and Software Tools for Parallel Processing, Vol. 26, No. 4, April 2000, pp. 293-314. pdf

Coglio, A,  A. Goldberg , and Z. Qian, “Towards a Provably-Correct Implementation of the JVM Bytecode Verifier,” Proc. DARPA Information Survivability Conference and Exposition (DISCEX`00), IEEE Computer Society Press, 403—410, Jan. 2000. Also
Proceedings of the OOPSLA '98 Workshop on the Formal Underpinnings of Java, Vancouver, B.C., October 1998. ps

Goldberg, A. “A Formalization of Java Bytecode Verifier and Loader," In the 5^Th ACM Conference on Communication and Computer Security, San Francisco, Nov. 1998. pdf

Coglio, A, A. Goldberg, and Z. Qian, “Towards a Provably-Correct Implementation of the JVM Bytecode Verifier,” OOPLSLA 1998 Workshop on the Formal Underpinnings of Java, Oct, 1998.  pdf

Goldberg, A. and T.C. Wang, “Integration of Linear Arithmetic and Goal-Oriented Resolution for Software Reasoning,” In Frontiers in Combining Systems, (FroCos ’98), Amsterdam, Netherlands, Oct. 1998.

Qian, X., Goldberg, A. “Bounds Analysis by Abstract Interpretation,” First Workshop on Automated Analysis of Programs, Paris, France, Jan., 1997.  pdf

Nyland, L. J. Prins, A. Goldberg, P. Mills, J. Reif, R. Wagner, “A Refinement Methodology for Data­Parallel Applications”, in Proc. EuroPar 96 Parallel Processing Conference, Lyon, France, LNCS 1123, Springer­Verlag, 1996 (pp 145-­151).

Goldberg, A., 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., Springer-Verlag, 1997. (40 pp)

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)  ps

Allen Goldberg, Rafael Furst, Cordell Green, A Refinement Approach to Visualization Kestrel Institute Technical Report KES.U.95.2, August 1995. pdf

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. pdf

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

Qian, X., Goldberg, A. “Referential Opacity in Non-Deterministic Data Refinement,”  ACM Letters on Programming Languages and Systems, Vol. 1-4, pp. 233-41, March 1993. pdf

Wang, T.C. and Goldberg, A., “RVF: An Automated Formal Verification System,” Proceedings of the 11th   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,” International Symposium on Software Reliability Engineering, Austin, TX, May 1991.

Blaine, L. and Goldberg, A. “ DTRE — A Semi-Automatic Transformation System,” Constructing Programs from Specifications. B. Möller, Ed., North Holland,1991.

Goldberg, A., “Reusing Software Developments,” Proceedings of the ACM SIGSOFT 4^th Symposium on Software Development Environments, December 1990. pdf

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., “Iteration in the Software Process,” Proceedings of the Third International Software Process Workshop, Breckenridge, Colorado, Nov. 1986.

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

Goldberg, A., “A Strategy for Semi-Automatic Program Development,” Invited paper, Nineteenth Annual Asilomar Conference on Circuits, Systems and Computers, November 1985.

Goldberg, A., and Pohl, I., “Is Complexity of Use to AI,” A. Elithorn and R. Banerji, Eds., Elsevier, 1984.

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

Goldberg, A., and Kotik, G., “Knowledge-Based Programming: An Overview of Data Structure Selection and Control Structure Refinement,” In Software Validation, H.L. Hausen, Ed., Elsevier, Amsterdam, 1984.

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., and Pohl, I., “Constraints of Complexity Computability,” Proceedings of the Second NATO Conference on Human and Artificial Thinking, 1981.

Goldberg, A., “On the Complexity of the Satisfiability Problem,” PhD thesis, Courant Institute, New York University, Report NSO-16, September 1979.

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