On Strings in Software Model Checking

作者: Hossein Hojjat , Philipp Rümmer , Ali Shamakhi

DOI: 10.1007/978-3-030-34175-6_2

关键词:

摘要: Strings represent one of the most common and intricate data-types found in software programs, with correct string processing often being a decisive factor for correctness security properties. This has led to wide range recent research results on how analyse programs operating strings, using methods like testing, fuzzing, symbolic execution, abstract interpretation, or model checking, and, increasingly, support strings is also added constraint solvers SMT solvers. In this paper, we focus verification checking. We give survey existing approaches handle context, propose based algebraic data-types, Craig interpolation, automata learning.

参考文章(41)
Richard Bubel, Reiner Hähnle, Ulrich Geilmann, A Formalisation of Java Strings for Program Specification and Verification Software Engineering and Formal Methods. ,vol. 7041, pp. 90- 105 ,(2011) , 10.1007/978-3-642-24690-6_8
Kamil Dudka, Petr Peringer, Tomáš Vojnar, Byte-Precise Verification of Low-Level List Manipulation static analysis symposium. pp. 215- 237 ,(2013) , 10.1007/978-3-642-38856-9_13
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman, None, Norn: An SMT Solver for String Constraints Computer Aided Verification. ,vol. 9206, pp. 462- 469 ,(2015) , 10.1007/978-3-319-21690-4_29
Abdulbaki Aydin, Lucas Bang, Tevfik Bultan, Automata-Based Model Counting for String Constraints Computer Aided Verification. pp. 255- 272 ,(2015) , 10.1007/978-3-319-21690-4_15
Margus Veanes, Symbolic String Transformations with Regular Lookahead and Rollback Lecture Notes in Computer Science. ,vol. 8974, pp. 335- 350 ,(2015) , 10.1007/978-3-662-46823-4_27
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
K. L. McMillan, Interpolation and SAT-Based Model Checking computer aided verification. pp. 1- 13 ,(2003) , 10.1007/978-3-540-45069-6_1
Vijay Ganesh, Adam Kieżun, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, Michael Ernst, HAMPI: a string solver for testing, analysis and vulnerability detection computer aided verification. pp. 1- 19 ,(2011) , 10.1007/978-3-642-22110-1_1
Bill Joy, James Gosling, Alex Buckley, Guy L. Steele, Gilad Bracha, The Java Language Specification, Java SE 8 Edition Addison-Wesley Professional. ,(2014)
Martin Rinard, Mia Minnes, Armando Solar-Lezama, Vijay Ganesh, What is Decidable about Strings ,(2011)