Project 305-CMU (1st year)
Software Modularity and Safety: Combining Model Checking and Theorem Proving
| We aim to investigate issues of program correctness and software safety from the perspective of modular software construction. We see model checkers and proof-assistance systems as two major tools in studying software modularity and safety. A model checker verifies a logic formula pertaining to certain safety property of a program against the program's all possible execution traces. Model checking can be automatic but often requires substantial computational resources for large systems. A proof assistant helps ensure certain safety property of a program by checking that its safety proof is sound. The proof can be constructed manually or automatically if the program has been properly annotated. A possible way to approach modular safety property is to use model checking at the component level, and to employ proof checking at the system level. |
| Specifically, we propose two projects that explore this combination. One is about compositional reasoning, and the other is about program analysis with separation logic. Compositional reasoning is a divide and conquer technique to verify hardware and software systems. |
| Assume-Guarantee Reasoning (AGR) is a form of compositional reasoning which allows us to break down the proof of system correctness in a compositional way into several sub-proofs. The sub-proofs involve showing guarantees on behaviors of a system component using, if necessary, assumptions about behaviors of other components in the system (the environment). We plan to investigate new circular AGR rules for compositionally verifying large software systems. |
| Separation logic has recently established itself as a useful technique for reasoning about programs that manipulate the heap, as it enables compositional reasoning even in the presence of heap operations. Reasoning about heap operations is desirable from a security standpoint, since many software security breaches are a result of improper manipulation of shared data structures in the heap. We propose extending our current automated tool so that it is able to make use of programmer-supplied annotations to break up and guide the verification problem. |
Member List
| Country | Organization | Full Name | Title | |
|---|---|---|---|---|
Taiwan |
TWISC |
Chuang, Tyng-Ruey |
PI |
|
Taiwan |
TWISC |
Wang, Bow-Yaw |
Co-PI |
|
Taiwan |
TWISC |
Tsay, Yih-Kuen |
Co-PI |
|
Taiwan |
TWISC |
Tsai, Chung-Hung |
Assistant |
|
Taiwan |
TWISC |
Tsai, Ming-Hsien |
Student |
|
Taiwan |
TWISC |
Chen, Yu-Fang |
Student |
|
US |
CMU |
Peter Lee |
Professor |
|
US |
CMU |
Ed Clarke |
Professor |
|
US |
CMU |
Stephen Magill |
Student |
|
US |
CMU |
Nishant Sinha |
Student |
Required documents (1st year)
Self-Assessment Presentation File (Internal Review Meeting)
Midterm Report (External Review Meeting)
Final Report (External Review Meeting)