Validation of correctness proofs is an established procedure in software verification. While there are steady advances when it comes to verification of more and more complex software systems, it becomes increasingly hard to determine which information is actually useful for validation of the correctness proof. Usually, the central piece that verifiers struggle to come up with are good loop invariants. While a proof using inductive invariants is easy to validate, not all invariants used by verifiers necessarily are inductive. In order to alleviate this problem, we propose LIV, an approach that makes it easy to check if the invariant information provided by the verifier is sufficient to establish an inductive proof. This is done by emulating a Hoare-style proof, splitting the program into Hoare triples and converting these into verification tasks that can themselves be efficiently verified by an off-the-shelf verifier. In case the validation fails, useful information about the failure reason can be extracted from the overview of which triples could be established and which were refuted. We show that our approach works by evaluating it on a state-of-the-art benchmark set. Demonstration video: https://youtu.be/mZhoGAa08Rk Reproduction package: https://doi.org/10.5281/zenodo.8289101
LIV Talk Slides (ASE2023_LIV_talk_slides.pdf) | 1.66MiB |
Thu 14 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | Program Verification 2Research Papers / Tool Demonstrations / NIER Track at Room E Chair(s): Martin Kellogg New Jersey Institute of Technology | ||
10:30 12mTalk | Expediting Neural Network Verification via Network Reduction Research Papers Yuyi Zhong National University of Singapore, Singapore, Ruiwei Wang School of Computing, National University of Singapore, Siau-Cheng Khoo National University of Singapore Pre-print File Attached | ||
10:42 12mTalk | SMT Solver Validation Empowered by Large Pre-trained Language Models Research Papers Maolin Sun Nanjing University, Yibiao Yang Nanjing University, Yang Wang National Key Laboratory for Novel Software Technology, Nanjing University, Ming Wen Huazhong University of Science and Technology, Haoxiang Jia Huazhong University of Science and Technology, Yuming Zhou Nanjing University Pre-print File Attached | ||
10:54 12mTalk | LIV: Invariant Validation Using Straight-Line Programs Tool Demonstrations Pre-print Media Attached File Attached | ||
11:06 12mTalk | CEGAR-PT: A Tool for Abstraction by Program Transformation Tool Demonstrations Pre-print Media Attached File Attached | ||
11:18 12mTalk | Symbolic Verification of Fuzzy Logic ModelsRecorded talk NIER Track Siang Zhao School of Computer, National University of Defense Technology, China, Zhongyang Li School of Computer, National University of Defense Technology, China, Zhenbang Chen National University of Defense Technology, Ji Wang School of Computer, National University of Defense Technology, China Pre-print Media Attached | ||
11:30 12mTalk | HOBAT: Batch Verification for Homogeneous Structural Neural NetworksRecorded talk Research Papers Media Attached File Attached |