PART_PW: From Partial Analysis Results to a Proof Witness

M.-C. Jakobs, in: A. Cimatti, M. Sirjani (Eds.), Software Engineering and Formal Methods, 2017, pp. 120–135.

Download
Restricted PARTMathrmPWFromPartialAnalysi.pdf 496.96 KB
Conference Paper | English
Author
Editor
;
Abstract
Today, verification tools do not only output yes or no, but also provide correctness arguments or counterexamples. While counterexamples help to fix bugs, correctness arguments are used to increase the trust in program correctness, e.g., in Proof-Carrying Code (PCC). Correctness arguments are well-studied for single analyses, but not when a set of analyses together verifies a program, each of the analyses checking only a particular part. Such a set of partial, complementary analyses is often used when a single analysis would fail or is inefficient on some program parts.We propose PART_PW, a technique which allows us to automatically construct a proof witness (correctness argument) from the analysis results obtained by a set of partial, complementary analyses. The constructed proof witnesses are proven to be valid correctness arguments and in our experiments we use them seamlessly and efficiently in existing PCC approaches.
Publishing Year
Proceedings Title
Software Engineering and Formal Methods
Page
120-135
LibreCat-ID

Cite this

Jakobs M-C. PART_PW: From Partial Analysis Results to a Proof Witness. In: Cimatti A, Sirjani M, eds. Software Engineering and Formal Methods. Lecture Notes in Computer Science. ; 2017:120-135. doi:10.1007/978-3-319-66197-1_8
Jakobs, M.-C. (2017). PART_PW: From Partial Analysis Results to a Proof Witness. In A. Cimatti & M. Sirjani (Eds.), Software Engineering and Formal Methods (pp. 120–135). https://doi.org/10.1007/978-3-319-66197-1_8
@inproceedings{Jakobs_2017, series={Lecture Notes in Computer Science}, title={PART_PW: From Partial Analysis Results to a Proof Witness}, DOI={10.1007/978-3-319-66197-1_8}, booktitle={Software Engineering and Formal Methods}, author={Jakobs, Marie-Christine}, editor={Cimatti, Alessandro and Sirjani, MarjanEditors}, year={2017}, pages={120–135}, collection={Lecture Notes in Computer Science} }
Jakobs, Marie-Christine. “PART_PW: From Partial Analysis Results to a Proof Witness.” In Software Engineering and Formal Methods, edited by Alessandro Cimatti and Marjan Sirjani, 120–35. Lecture Notes in Computer Science, 2017. https://doi.org/10.1007/978-3-319-66197-1_8.
M.-C. Jakobs, “PART_PW: From Partial Analysis Results to a Proof Witness,” in Software Engineering and Formal Methods, 2017, pp. 120–135.
Jakobs, Marie-Christine. “PART_PW: From Partial Analysis Results to a Proof Witness.” Software Engineering and Formal Methods, edited by Alessandro Cimatti and Marjan Sirjani, 2017, pp. 120–35, doi:10.1007/978-3-319-66197-1_8.
Main File(s)
File Name
PARTMathrmPWFromPartialAnalysi.pdf 496.96 KB
Access Level
Restricted Closed Access
Last Uploaded
2018-11-02T14:47:04Z


Export

Marked Publications

Open Data LibreCat

Search this title in

Google Scholar