عنوان
پدید آورنده
موضوع
رده
کتابخانه
محل استقرار
TLpq2382093893
انگلیسی
A Logical Analysis of Relational Program Correctness
[Thesis]
Nikouei, Mohammad
Naumann, David A
Stevens Institute of Technology
2019
178
Ph.D.
Stevens Institute of Technology
2019
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
مطالعه متن کتاب p
[Thesis]
276903
a
Y
