23-Sep-2015: 5th Linux Driver Verification Workshop took place in Moscow
5th Linux Driver Verification Workshop dedicated to the 10th anniversary of the Linux Verification Center of ISPRAS was held in Moscow, Russia on September 15-18. The workshop was arranged by prof. Alexander Petrenko (Linux Verification Center, ISPRAS, Moscow, Russia) and prof. Dirk Beyer (University of Passau, Germany).
Alexey Khoroshilov has opened 5th Linux Driver Verification Workshop and highlighted the main achievements of CPAchecker regarding its usage in Linux Driver Verification project. He concluded that BLAST is still useful as an additional tool, but CPAchecker finally became the main verifier for the LDV project.
Dirk Beyer presented talk "Witness Validation and Stepwise Testification across Software Verifiers" where he described the methods for checking the results of one software verifier by the other verifiers. Also he has shown the benefits of search-space reduction and the possibilities for efficient and effective combinations of techniques.
The power of sequential combinations of different approaches was demonstrated by Vadim Mutilin. He has found several configurations where CPAchecker has better results on Linux device drivers than the current one. In the talk he discussed the current state of using CPAchecker without CIL and the problem of nondeterministic behavior.
Vitaly Mordan has described an approach for checking several properties at once which significantly speeds up the analysis with almost the same results as in checking properties one by one separately.
Andreas Stahlbauer gave a talk "Multi-Property Verification Using Precision Control" discussing the same problems as Vitaly with an emphasis on formalization in context of Configurable Program Analysis (CPA). Has concluded that costs for software model checking do not necessarily explode with a growing number of properties.
In addition Vitaly gave a talk on "Finding Several Bugs at Once" where verification tool does not stop after the first violation is identified, but it continues to find other violations of the same property until all of them are found. This approach leads to enormous amount of error traces corresponding to the same bugs and Vitaly presented a method of clustering the error traces that allows to reduce efforts required to analyze them.
Pavel Andrianov has discussed problems and perspectives of Block Abstraction Memorization (BAM). The problems were concerned with such parts of BAM as partitioning building, path computing, ARG cleaning, aggressive predicate reduction etc.
In the talk "Theory-Independent Reuse of Abstraction Formulas: Towards Proof Reuse" Karlheinz Friedberger has presented approaches for reusing formulas from an analysis with linear integer arithmetics to analysis with bit-vectors and converting formulas between theories, striving to
make bit-precise verification of programs faster.
Sebastian Ott presented "A Web-Interface for the CPAchecker Cloud" allowing parallel verification of large number of tasks with accurate and reproducible results. The Cloud is successfully used in development of CPAchecker and significantly speeds up implement-test-roundtrip time.
Anton Vasilyev has talked about checking memory safety for the Linux kernel. He identified a number of issues in the current SMGCPA approach which was used at the International Software Verification Competition (SV-COMP'15) and suggested possible solutions.
Ilya Zakharov has investigated CPAchecker bottlenecks on Linux device drivers and presented results of experiments and its classification for different CPAchecker configurations. Mikhail Mandrykin has highlighted the directions for improvements of memory model in CPAchecker. Vitaly Mordan provided the results of first experiments with complex specifications based on CPAchecker property automaton.
Dirk Beyer gave the talk "Boosting k-Induction with Continuously-Refined Invariants" presenting an approach of extending Bounded Model Checking (BMC) towards unbounded safety proofs.
Altogether the teams discussed open questions and action items for the future work.
