PRoofster: Automated Formal Verification

被引：1

作者：

Agrawal, Arpan ^{[1
]}

First, Emily ^{[2
]}

Kaufman, Zhanna ^{[2
]}

Reichel, Tom ^{[1
]}

Zhang, Shizhuo ^{[1
]}

Zhou, Timothy ^{[1
]}

Sanchez-Stern, Alex ^{[2
]}

Ringer, Talia ^{[1
]}

Brun, Yuriy ^{[2
]}

机构：

[1] Univ Illinois, Urbana, IL 61801 USA

[2] Univ Massachusetts, Amherst, MA 01003 USA

来源：

2023 IEEE/ACM 45TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: COMPANION PROCEEDINGS, ICSE-COMPANION | 2023年

基金：

美国国家科学基金会;

关键词：

D O I：

10.1109/ICSE-Companion58688.2023.00018

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Formal verification is an effective but extremely work-intensive method of improving software quality. Verifying the correctness of software systems often requires significantly more effort than implementing them in the first place, despite the existence of proof assistants, such as Coq, aiding the process. Recent work has aimed to fully automate the synthesis of formal verification proofs, but little tool support exists for practitioners. This paper presents PRoofster, a web-based tool aimed at assisting developers with the formal verification process via proof synthesis. PRoofster inputs a Coq theorem specifying a property of a software system and attempts to automatically synthesize a formal proof of the correctness of that property. When it is unable to produce a proof, PRoofster outputs the proof-space search tree its synthesis explored, which can guide the developer to provide a hint to enable PRoofster to synthesize the proof. PRoofster runs online at https://proofster.cs.umass.edu/ and a video demonstrating PRoofster is available at https://youtu.be/xQAi66lRfwI/.

引用

页码：26 / 30

页数：5

共 54 条

[1] SOSRepair: Expressive Semantic Search for Real-World Program Repair
Afzal, Afsoon
Motwani, Manish
Stolee, Kathryn T.
Brun, Yuriy
Le Goues, Claire
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2021, 47 (10) : 2162 - 2181
[2] FairSquare: Probabilistic verification of program fairness
Albarghouthi A.
D’Antoni L.
Drews S.
Nori A.V.
[J]. Proceedings of the ACM on Programming Languages, 2017, 1 (OOPSLA)
[3] Themis: Automatically Testing Software for Discrimination
Angell, Rico
Johnson, Brittany
Brun, Yuriy
Meliou, Alexandra
[J]. ESEC/FSE'18: PROCEEDINGS OF THE 2018 26TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING, 2018, : 871 - 875
[4] js']jsCoq: Towards Hybrid Theorem Proving Interfaces
Arias, Emilio Jesus Gallego
Pin, Benoit
Jouvelot, Pierre
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (239): : 15 - 27
[5] aws.amazon, AWS PROV SEC
[6] Blaauwbroek L., 2020, EPiC Series in Computing, V73, P138, DOI [10.29007/wg1q, 10.]
[7] Bostock M., 2012, D3.js - data-driven documents
[8] Software Fairness
Brun, Yuriy
Meliou, Alexandra
[J]. ESEC/FSE'18: PROCEEDINGS OF THE 2018 26TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING, 2018, : 754 - 759
[9] Chen ZP, 2024, Arxiv, DOI arXiv:2207.10223
[10] A Type System for Privacy Properties
Cortier, Veronique
Grimm, Niklas
Lallemand, Joseph
Maffei, Matteo
[J]. CCS'17: PROCEEDINGS OF THE 2017 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, 2017, : 409 - 423

← 1 2 3 4 5 6 →