Mike Czech
ABSTRACT
Today, software verification tools have reached the maturity to be used for large scale programs. Different tools perform differently well on varying code. A software developer is hence faced with the problem of choosing a tool appropriate for her program at hand. A ranking of tools on programs could facilitate the choice. Such rankings can, however, so far only be obtained by running all considered tools on the program.
In this paper, we present a machine learning approach to predicting rankings of tools on programs. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for programs. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from the software verification competition SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy (rank correlation > 0.6).
- Dirk Beyer. 2015. Software Verification and Verifiable Witnesses - (Report on SVCOMP 2015). In TACAS (LNCS), Christel Baier and Cesare Tinelli (Eds.), Vol. 9035.Google Scholar
- Springer, 401–416.Google Scholar
- Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, and Farn Wang. 2016. PAC learning-based verification and model synthesis. In ICSE, Laura K. Dillon, Willem Visser, and Laurie Williams (Eds.). ACM, 714–724. Google ScholarDigital Library
- A. Corazza, S. Di Martino, V. Maggio, and G. Scanniello. 2010.Google Scholar
- A Tree Kernel based approach for clone detection. In ICSM. IEEE, 1–5.Google Scholar
- Yulia Demyanova, Thomas Pani, Helmut Veith, and Florian Zuleger. 2015. Empirical Software Metrics for Benchmarking of Verification Tools. In CAV (LNCS), Daniel Kroening and Corina S. Pasareanu (Eds.), Vol. 9206. Springer, 561–579. Google ScholarCross Ref
- Susan Horwitz and Thomas W. Reps. 1992.Google Scholar
- The Use of Program Dependence Graphs in Software Engineering. In ICSE, Tony Montgomery, Lori A. Clarke, and Carlo Ghezzi (Eds.). ACM Press, 392–411.Google Scholar
- E. Hüllermeier, J. Fürnkranz, W. Cheng, and K. Brinker. 2008. Label Ranking by Learning Pairwise Preferences. Artificial Intelligence 172 (2008), 1897–1917. Google ScholarDigital Library
- Wenchao Li, Hassen Saidi, Huascar Sanchez, Martin Schäf, and Pascal Schweitzer. 2016. Detecting Similar Programs via The Weisfeiler-Leman Graph Kernel. In Software Reuse: Bridging with Social-Awareness (LNCS), Georgia M. Kapitsaki and Eduardo Santana de Almeida (Eds.), Vol. 9679. Springer, 315–330. Google ScholarDigital Library
- Tim Menzies and Thomas Zimmermann. 2013. Software Analytics: So What? IEEE Software 30, 4 (2013), 31–37. Google ScholarDigital Library
- Justin Sahs and Latifur Khan. 2012. A Machine Learning Approach to Android Malware Detection. In EISIC, Nasrullah Memon and Daniel Zeng (Eds.). IEEE Computer Society, 141–147. Google ScholarDigital Library
- B. Schölkopf and AJ. Smola. 2001.Google Scholar
- Learning with Kernels: Support Vector Machines, Regularization, Optimization, and Beyond. MIT Press.Google Scholar
- Nino Shervashidze, Pascal Schweitzer, Erik Jan van Leeuwen, Kurt Mehlhorn, and Karsten M. Borgwardt. 2011. Weisfeiler-Lehman Graph Kernels. Journal of Machine Learning Research 12 (2011), 2539–2561.Google ScholarDigital Library
- Varun Tulsian, Aditya Kanade, Rahul Kumar, Akash Lal, and Aditya V. Nori. 2014.Google Scholar
- MUX: algorithm selection for software model checkers. In MSR, Premkumar T. Devanbu, Sung Kim, and Martin Pinzger (Eds.). ACM, 132–141.Google Scholar
- Boris Weisfeiler and A.A. Lehman. 1968. A reduction of a graph to a canonical form and an algebra arising during this reduction. Nauchno Technicheskaya Informatsia 2, 9 (1968), 12–19.Google Scholar
- Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. 2008. SATzilla: Portfolio-based Algorithm Selection for SAT. J. Artif. Intell. Res. (JAIR) 32 (2008), 565–606. Abstract 1 Introduction 2 Representing Verification Tasks 3 Predicting Rankings 3.1 Label Ranking 3.2 Ranking by Pairwise Comparison 3.3 Graph Kernels for Verification Tasks 4 Experimental Evaluation 5 Conclusion ReferencesGoogle ScholarCross Ref
Index Terms
- Predicting rankings of software verification tools
Recommendations
What's Going on in Search Engine Rankings?
AINAW '08: Proceedings of the 22nd International Conference on Advanced Information Networking and Applications - WorkshopsMany people use search engines every day to retrieve documents from the Web. Although the social influence of search engine rankings has become significant, ranking algorithms are not disclosed. In this paper, we have investigated three major search ...
Comparing rankings of search results on the Web
Special issue: InfometricsThe Web has become an information source for professional data gathering. Because of the vast amounts of information on almost all topics, one cannot systematically go over the whole set of results, and therefore must rely on the ordering of the results ...
Software Verification Tools (Track Introduction)
Leveraging Applications of Formal Methods, Verification and Validation: Tools and TrendsAbstractThis ISoLA track is concerned with methods for the evaluation and comparison of analysis and verification techniques: we discuss conservative static-analysis and verification tools, as well as discuss and evaluate state-of-the-art approaches. As ...
Comments