Software Verification with PDR: An Implementation of the State of the Art
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 22 | |
| Author | ||
| Contributors | ||
| License | CC Attribution 3.0 Germany: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/55015 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
| |
| Keywords |
00:00
SoftwareFormal verificationImplementationInvariantentheorieObservational studyInvariant (mathematics)Inductive reasoningCategory of beingComputer hardwareBefehlsprozessorProof theoryTask (computing)Limit (category theory)Pairwise comparisonCompilation albumComputer programOpen sourceDisintegrationBenchmarkAlgorithmFormal verificationSet (mathematics)Observational studyInvariantentheorieCodeImplementationPresentation of a groupNumberSoftware frameworkElectronic design automationState transition systemComputer programSoftwareTable (information)Invariant (mathematics)QuantilePlotterCASE <Informatik>ResultantComponent-based software engineeringOpen sourceINTEGRALRepository (publishing)Slide ruleWeb pageOpen setDiagram
Transcript: English(auto-generated)
00:00
Welcome! This presentation provides an overview over an implementation of the state-of-the-art in software verification with PDR. PDR is short for Property Driven Reachability. This is a verification algorithm that is extremely successful in hardware verification.
00:22
And we implement an adoption to software verification. My name is Dirk Bayer. I am from LMU Munich in Germany and this is joint work with Matthias Dangel. The contributions of the paper are the following. We implemented an adoption of PDR to software verification in the open source verification framework CPA Checker.
00:47
This makes it possible to thoroughly study the performance of this approach on practical problems. We design and implement the invariant generator KI-PDR, which can be used as an invariant generator, for example in K-induction approaches.
01:06
We perform a large experimental study to compare several tools that use PDR as a component. We provide a set of example programs that illustrate the strength of PDR on code that is conveniently small to look at.
01:25
Next, I would like to mention some of our background. Our work is based on the seminal work of Aaron Bradley. This algorithm for verification of transition systems received a lot of attention and is extremely successful in hardware verification.
01:42
There are several adoptions to software, which are all unfortunately not available or not competitive. We implement and improve the adoption of PDR to software, which is called C-Tiger from TU-VNR.
02:04
Our approach for a full verification approach is to integrate PDR into K-induction, where PDR serves as an invariant generation engine. Finally, we compare our approach with the tools VVT and C-Horn, for which the results can be reproduced.
02:26
This presentation is too short to explain how PDR works, but there are nice explanations available, for example in our paper or in other presentations. I would like to report about our evaluation. First, we want to know whether our implementation works and is efficient.
02:47
We compare our implementation of C-Tiger with the Vienna implementation. The quantile plot shows that our implementation solves more tasks, which is good news.
03:02
Second, we compare the PDR-based invariant generator with three other invariant generators. We use small handcrafted examples to illustrate the strengths of PDR. On those examples, K-induction without an auxiliary invariant generator does not succeed.
03:20
The table shows that only the PDR-based approach can deliver invariants for all of the examples. Third, we compare with the six verifiers from SVComp that performed best on the examples. We contributed the examples to the benchmark set that is used for SVComp, so the results are available publicly already.
03:52
The table shows that PDR is pretty robust, while other approaches struggle for some cases.
04:02
Last but not least, we compare the two other available tools that use PDR. Those are VVT and C-Horn. The quantile plots illustrate that C-Horn produces a large number of wrong results,
04:20
while our approach with PDR in K-induction is slow but more effective. To conclude, we provide to the research community an implementation of PDR4 software. It is open source, reproducible, competitive, and integrated in the state-of-the-art verification framework, namely CPA Checker.
04:47
In sum, this is a reference implementation that can be used by others to study PDR4 software. The invariant generation component is usable also in other contexts.
05:01
The results are reproducible because all components are available in the artifact and also in the code repository of CPA Checker. Thank you for your interest in PDR4 software. This ends my presentation. I added the references to the end of the slides and this is the end of my presentation.
05:27
The set of slides is available on my webpage.