Research Projects

I have started my PhD studies in January 2002. Since then, my research focused on the ares of program analysis, programming languages and software engineering. More specifically, I have worked on the following topics:

Proving Program Safety and Bug Finding

Showed how to use disjunctive fixed-point analysis to support either proofs of program safety or bug finding. Proposed a dual static analysis based only on over-approximation and validated its capabilities with a set of experiments [10]. Formalized and proved the analysis correctness [9].

Software: Uses the Omega Library. (Linux x86 executable, Sample input files, web demo)

Disjunctive Invariants for Static Analysis

Designed a new disjunctive numerical abstract domain adapting hulling and widening operators from the polyhedron domain to its disjunctive domain extension. The resulting fixed-point analysis was used to compute precise method postconditions [3] and preconditions [2]. These techniques are further elaborated in my thesis [9].

Software: Available from the CVS repository in loris-7 server: /home/popeeaco/cvs-repository/array-code. (web demo, fixpoint calculator)

Memory Bounds Inference

Contributed to the design of an analysis to infer bounds for the memory needed to execute low-level programs [1]. The prototype system is based on the disjunctive fixed-point analysis introduced in [3].

Software: Available from the CVS repository in loris-7 server: /home/popeeaco/cvs-repository/stack-code/ : /home/popeeaco/cvs-repository/memory-examples/.

Genericity for Java

Contributed to the design of a flow-based technique for capturing generic types in Java [4]. A prototype system was applied to a suite of Java applications and more casts could be proven safe compared to using wildcard-generic Java 1.5.

Resource Usage Verification

Designed a dependent type system for checking the correct usage of resources in the context of a first-order functional language [6]. The dependent type system was extended with alias checking and applied to object-based programs with customized safety policies [5]. An algorithm was proposed to infer alias annotations for our object-based language [11]. An intern student has developed a type checker for a simple functional language.

Software (developed by Ana Oprescu): Available from the CVS repository in loris-7 server: /home/popeeaco/cvs-repository/resources-code/.

CIL2IMP Translator

This project proposes a new core language for C that is expression-oriented. The main focus of this core language is to support easier program analysis.

Software (under development) : Available from the SVN repository in loris-7 server: /home/popeeaco/svn-repositories/cil2imp-code/ (preliminary report, online documentation, code via Trac).

Octagon and PPL interfaces

An intern student has used the Haskell language to develop interfaces to the Octagon library and the PPL (Parma Polyhedra Library).

Software (developed by Ramona Bobohalma): Available from the CVS repository in loris-7 server: /home/popeeaco/cvs-repository/octagon-code/ : /home/popeeaco/cvs-repository/ppl-code/.

Omega Library interface

An intern student has used the Haskell language to develop an interface to the Omega Library interface.

Software (developed by Razvan Musaloiu): Available from the CVS repository in loris-7 server: /home/popeeaco/cvs-repository/omega_stub/.

List of publications

  1. Wei-Ngan Chin, Huu Hai Nguyen, Corneliu Popeea, Shengchao Qin - Analysing Memory Resource Bounds for Low-Level Programs. ACM International Symposium on Memory Management, ISMM 2008.
  2. Corneliu Popeea, Dana N. Xu, Wei-Ngan Chin - A Practical and Precise Inference and Specializer for Array Bound Checks Elimination. ACM Partial Evaluation and Program Manipulation, PEPM 2008. Acceptance Rate: 27% (20 papers accepted / 74 submissions).
  3. Corneliu Popeea, Wei-Ngan Chin - Inferring Disjunctive Postconditions. Asian Computer Science Conference, ASIAN 2006. Acceptance Rate: 15% (17 papers accepted / 115 submissions).
  4. Wei-Ngan Chin, Florin Craciun, Siau-Cheng Khoo, Corneliu Popeea - A Flow-Based Approach for Variant Parametric Types. ACM International Conference on Object-Oriented Programming, Systems, Languages and Applications, OOPSLA 2006. Acceptance Rate: 16% (26 papers accepted / 157 submissions).
  5. Wei-Ngan Chin, Siau-Cheng Khoo, Shengchao Qin, Corneliu Popeea, Huu Hai Nguyen - Verifying Safety Policies with Size Properties and Alias Controls. ACM/IEEE International Conference on Software Engineering, ICSE 2005. Acceptance Rate: 14% (44 papers accepted / 313 submissions).
  6. Corneliu Popeea, Wei-Ngan Chin - A Type System for Resource Protocol Verification and its Correctness Proof. ACM Partial Evaluation and Program Manipulation, PEPM 2004. Acceptance Rate: 44% (13 papers accepted / 29 submissions).

    7. POSTERS
  7. Florin Craciun, Hong Yaw Goh, Corneliu Popeea, Wei-Ngan Chin - Core-Java: An Expression-Oriented Java. Poster paper published in the Companion to the Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006.
  8. Florin Craciun, Corneliu Popeea, Siau-Cheng Khoo, Wei-Ngan Chin - Flow Analysis for Variant Parametric Types in Java. Poster presented at the Asian Symposium on Programming Languages and Systems, APLAS 2005.

    9. THESIS
  9. Corneliu Popeea – Disjunctive Invariants for Modular Static Analysis. Ph.D. thesis. Available at http://www.model.in.tum.de/~popeea/research/thesis.pdf

    10. UNPUBLISHED REPORTS
  10. Corneliu Popeea, Wei-Ngan Chin - Dual Analysis for Proving Safety and Finding Bugs. Submitted for publication.
  11. Huu Hai Nguyen, Corneliu Popeea – Uniqueness Inference for Object-Oriented Languages. Technical report available at http://www.model.in.tum.de/~popeea/research/uniqueness.tr.pdf
  12. Corneliu Popeea – Deriving Safety Pre-Condition for Array Bounds Check in Imperative Programs. Report on the final year project, 2001.