عنوان

A Logical Analysis of Relational Program Correctness

Number

TLpq2382093893

.Language of Text, Soundtrack etc

انگلیسی

Title Proper

A Logical Analysis of Relational Program Correctness

General Material Designation

[Thesis]

First Statement of Responsibility

Nikouei, Mohammad

Subsequent Statement of Responsibility

Naumann, David A

Name of Publisher, Distributor, etc.

Stevens Institute of Technology

Date of Publication, Distribution, etc.

2019

Specific Material Designation and Extent of Item

178

Dissertation or thesis details and type of degree

Ph.D.

Body granting the degree

Stevens Institute of Technology

Text preceding or following the note

2019

Text of Note

Precise mathematical specifications of software requirements and rigorous verification of correctness is a challenging problem. Automating this process by means of first-order theorem provers is even more difficult. The requirements of interest in this work include so-called relational properties that involve relating two executions of two possibly different programs. Secure information flow, correctness of compiler optimizations, and program revisions such as refactoring and changed data representations are some interesting relational properties. For effective requirements specification and automated reasoning about object-oriented programs, specs and proofs should be composed modularly, in accord with program structure and locality of dynamic data structures. Encapsulation is essential to reduce coupling between components and their proofs, but is difficult to achieve due to sharing of mutable objects: It is hard to give precise semantics of encapsulation that is flexible enough to handle software design patterns, strong enough to enable modular reasoning, and simple enough to be expressed in the first-order formulas supported by automated provers. Modular verification of relational properties also requires alignment of similar subprograms to maximize opportunities for simple intermediate assertions. This thesis introduces a subtle semantics of dependency and read effects, and on that basis develops a powerful semantics of encapsulation, augmenting prior work on Region Logic to provide for relational verification. A program logic as a deductive system is introduced for relational verification, with rules that embody the principles of local and modular reasoning; this includes weaving related code together to designate alignment points, and the key notion of second order framing which enables sound information hiding in module interface specifications. All rules of the program logic have been proved sound. They have also been implemented in an automated program verifier which checks specifications provided by the user, against woven programs generated according to alignment hints also provided by the user. The verifier directly implements some of the proof rules but is mainly based on generating verification conditions that are checked by an automated prover. The verifier has been evaluated through example verifications including challenge problems in relational verification, such as differing implementations of the union-find interface, for which Kruskal's algorithm is a client.

Computer science

Naumann, David A

Nikouei, Mohammad

Electronic name

p

[Thesis]

276903

a

Y