Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


Thesis.pdf (9.5 MB)

ETD Abstract Container

Abstract Header

A Balanced Verification Effort for the Java Language

Zaccai, Diego Sebastian
http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619

Abstract Details

2016, Doctor of Philosophy, Ohio State University, Computer Science and Engineering.
Current tools used to verify software in languages with reference semantics, such as Java, are hampered by the possibility of aliases. Existing approaches to addressing this long-standing verification problem try not to sacrifice modularity because modular reasoning is what makes verification tractable. To achieve this, these approaches treat the value of a reference variable as a memory address in the heap. A serious problem with this decision is that it severely limits the usefulness of generic collections because they must be specified as collections of references, and components of this kind are fundamentally flawed in design and implementation. The limitations become clear when attempting to verify clients of generic collections. The first step in rectifying the situation is to redefine the "value" of a reference variable in terms of the abstract value of the object it references. A careful analysis of what the "value" of a reference variable might mean leads inevitably to this conclusion, which is consistent with the denotation of a variable in languages with value semantics, such as RESOLVE. Verification in languages with value semantics is straightforward compared to verification in languages with reference semantics precisely because of the lack of concern with heap properties. However, there is still a nagging problem: aliasing can occur in legal programs in languages with reference semantics, such as Java, and it must be handled when it does occur. The crux of the issue is not in-your-face assignment statements that copy references but rather aliasing arising within (hidden) method bodies. The reason is that the effects of calls to these methods in client code must be summarized in their specifications in order to preserve modularity. So, the second step is the introduction of a discipline restricting what a client can do with a reference that is aliased within a method. The discipline advertises the creation of such aliases in method specifications and prevents a client from engaging in behavior that would break the abstractions of the objects being referenced, as this would also prevent modular verification. These restrictions allow code to be specified in terms of the abstract values of objects instead of treating the values of references as memory addresses in the heap. Even though the discipline prevents some programming idioms, it remains flexible enough to allow for most common programs, including the use of iterators, without the need for workarounds. A tool can verify that a program satisfies the provisions of this discipline. Further, it can generate verification conditions that rely only on abstract object values to demonstrate a program's correctness. These verification conditions can be discharged by the theorem-proving tools currently used to verify RESOLVE programs.
Bruce W. Weide (Advisor)
Neelam Soundarajan (Committee Member)
Paul A. G. Sivilotti (Committee Member)
221 p.
Computer Science
Formal Methods; Software Verification

Recommended Citations

Citations

  • Zaccai, D. S. (2016). A Balanced Verification Effort for the Java Language [Doctoral dissertation, Ohio State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619

    APA Style (7th edition)

  • Zaccai, Diego. A Balanced Verification Effort for the Java Language. 2016. Ohio State University, Doctoral dissertation. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619.

    MLA Style (8th edition)

  • Zaccai, Diego. "A Balanced Verification Effort for the Java Language." Doctoral dissertation, Ohio State University, 2016. http://rave.ohiolink.edu/etdc/view?acc_num=osu1461243619

    Chicago Manual of Style (17th edition)

osu1461243619
860
© 2016, all rights reserved.
This open access ETD is published by The Ohio State University and OhioLINK.