Activity
Time:
Ph.D. Thesis Defense: Guolong Zheng
Date:
11:00 am –
12:00 pm
Zoom Room: https://unl.zoom.us/j/96776285002
Ph.D. Thesis Defense: Guolong Zheng
“Ensure Correctness For Imperative and Declarative Programs”
There are two different types of programs: imperative program that describes how to solve a problem and declarative program that describes how to recognize that the problem is solved. The inherent difference between them leads to different analysis techniques. In this dissertation, we develop tools to ensure correctness and improve reliability for both imperative and declarative programs. For imperative program, we focus on automatically infer program invariant. Program invariant, which describes program states or behaviors as mathematical formulas, is one main approach to verify and debug imperative programs. However, current invariant generation techniques focus on numerical invariant described by Hoare Logic, lacking support for memory related properties. We present SLING, a dynamic analysis tool to automatically infer program invariant described by Separation Logic, an extension of Hoare logic with compact description for memory properties. The empirical results show that SLING can efficiently discover invariant for pointers and data structures and the generated invariant can be used automatically repair corrupted data structures. For declarative program, we focus on automatically debugging Alloy specifications. Alloy is a declarative specification language widely used in various software problems. However, unlike imperative programs, there is a dearth of techniques to help debugging Alloy specifications. We present FLACK to automatically locate Alloy bugs and ATR to repair them. Experimental results show that FLACK can accurately locate buggy expressions and ATR can effectively repair different types of bugs.
Committe Members:
ThanhVu Nguyen, Advisor
Hamid Bagheri, Co-Advisor
Lisong Xu
Matthew Dwyer
Shane Farritor
“Ensure Correctness For Imperative and Declarative Programs”
There are two different types of programs: imperative program that describes how to solve a problem and declarative program that describes how to recognize that the problem is solved. The inherent difference between them leads to different analysis techniques. In this dissertation, we develop tools to ensure correctness and improve reliability for both imperative and declarative programs. For imperative program, we focus on automatically infer program invariant. Program invariant, which describes program states or behaviors as mathematical formulas, is one main approach to verify and debug imperative programs. However, current invariant generation techniques focus on numerical invariant described by Hoare Logic, lacking support for memory related properties. We present SLING, a dynamic analysis tool to automatically infer program invariant described by Separation Logic, an extension of Hoare logic with compact description for memory properties. The empirical results show that SLING can efficiently discover invariant for pointers and data structures and the generated invariant can be used automatically repair corrupted data structures. For declarative program, we focus on automatically debugging Alloy specifications. Alloy is a declarative specification language widely used in various software problems. However, unlike imperative programs, there is a dearth of techniques to help debugging Alloy specifications. We present FLACK to automatically locate Alloy bugs and ATR to repair them. Experimental results show that FLACK can accurately locate buggy expressions and ATR can effectively repair different types of bugs.
Committe Members:
ThanhVu Nguyen, Advisor
Hamid Bagheri, Co-Advisor
Lisong Xu
Matthew Dwyer
Shane Farritor