Verifying object construction

Martin Kellogg, Manli Ran, Manu Sridharan, Martin Schaf, Michael D. Ernst

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Scopus citations


In object-oriented languages, constructors often have a combination of required and optional formal parameters. It is tedious and inconvenient for programmers to write a constructor by hand for each combination. The multitude of constructors is error-prone for clients, and client code is difficult to read due to the large number of constructor arguments. Therefore, programmers often use design patterns that enable more flexible object construction-the builder pattern, dependency injection, or factory methods. However, these design patterns can be too flexible: not all combinations of logical parameters lead to the construction of wellformed objects. When a client uses the builder pattern to construct an object, the compiler does not check that a valid set of values was provided. Incorrect use of builders can lead to security vulnerabilities, run-time crashes, and other problems. This work shows how to statically verify uses of object construction, such as the builder pattern. Using a simple specification language, programmers specify which combinations of logical arguments are permitted. Our compile-time analysis detects client code that may construct objects unsafely. Our analysis is based on a novel special case of typestate checking, accumulation analysis, that modularly reasons about accumulations of method calls. Because accumulation analysis does not require precise aliasing information for soundness, our analysis scales to industrial programs. We evaluated it on over 9 million lines of code, discovering defects which included previously-unknown security vulnerabilities and potential null-pointer violations in heavily-used open-source codebases. Our analysis has a low false positive rate and low annotation burden. Our implementation and experimental data are publicly available.

Original languageEnglish (US)
Title of host publicationProceedings - 2020 ACM/IEEE 42nd International Conference on Software Engineering, ICSE 2020
PublisherIEEE Computer Society
Number of pages12
ISBN (Electronic)9781450371216
StatePublished - Jun 27 2020
Externally publishedYes
Event42nd ACM/IEEE International Conference on Software Engineering, ICSE 2020 - Virtual, Online, Korea, Republic of
Duration: Jun 27 2020Jul 19 2020

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257


Conference42nd ACM/IEEE International Conference on Software Engineering, ICSE 2020
Country/TerritoryKorea, Republic of
CityVirtual, Online

All Science Journal Classification (ASJC) codes

  • Software


  • Ami sniping
  • Autovalue
  • Builder pattern
  • Lightweight verification
  • Lombok
  • Pluggable type systems


Dive into the research topics of 'Verifying object construction'. Together they form a unique fingerprint.

Cite this