Efficient software model checking with block-abstraction memoization

Friedberger, Karlheinz (2021): Efficient software model checking with block-abstraction memoization. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

The increasing availability of information technology in today’s life is a challenge for users as well as for engineers. The execution of a myriad of machine operations per second on each single device as well as world-wide communication between applications in research, industry, and personal domain require reliability and scalability of computer systems, both on hardware and software level. Increasing complexity as well as a big potential for errors make it challenging to develop and maintain such systems. This causes failures in applications, reaching from simple blue screens on personal computers towards accidents in critical infrastructure, such as crashing airplanes and invalid settings for medical equipment, affecting a large number of people. To address this challenge, it becomes more and more important to use processes to avoid failures in new software and find bugs in already exiting software. Prominent approaches used in quality management of critical systems are formal methods like formal verification and especially model checking, which aims at proving whether a system meets a given specification and fulfills its requirements. Researchers and developers use formal verification for a wide area of applications, including hardware-circuit designs, flight-control systems, and even operating-system drivers that run in everyone’s computer. In the last decades, the research community has made several steps towards better usage, adaptation, and understanding of formal techniques. However, due to their high demand of resources in both manpower as well as computational effort, formal methods are still not as used in the standard software development process as plain testing, but almost exclusively in critical applications, where a failure can get life-threatening or disproportionately expensive. To fulfill the high demand and large-scale availability of quality management, formal verification needs to run automatically and with only small amount of manpower. With our research in this context, we considered the following challenges: - To enable smaller teams with larger software projects to use formal methods, we need scalable and modular software-verification approaches that not only aim for a lower amount of required resources, but also use the available resources efficiently and allow for caching and reuse of partial analysis results. - To analyze parallel running software systems with e. g. communicating components, we need a simple formalism and verification technique for parallel systems that works in a domain-independent way, such that several already existing analyses can be applied easily. - To allow software developers to use model-checking tools regularly, we need to improve the usability and exported data of suchlike, e. g., with using a standardized file format for exchanging analysis results between tools. - To support the development of new verification approaches and other applications based on formal theory, we need to improve the usability of often-used backend components for solving constraints and analyzing formulas, such as providing simple interfaces and ready-to-use libraries for SMT solvers. The basis for our research is the open-source verification framework CPAchecker, which provides a convenient context to declare program analyses, supports multiple abstract domains for encoding program behavior, and already contains several approaches and algorithms for software verification. Our studies on scalable and modular approaches show the potential of block-abstraction memoization, which is a verification technique based on a divide-and-conquer strategy that leverages the internal structure of a program. Using an abstract domain like predicate abstraction, value analysis, or combinations thereof, we evaluate the approach on a large and established benchmark set to provide evidence for its competitive performance against other state-of-the-art approaches and also to show that CPUs with multiple cores can be used to their full potential. Our research on parallel systems enables interesting insights into multi-threaded verification tasks. We develop a theoretical approach to handle concurrency in a simple, but efficient and also domain-independent way, and provide the corresponding implementation in CPAchecker. Additionally, the established standardized format for the representation of verification witnesses is extended with additional information about the concurrent context and thread scheduling which are valuable artifacts from the verification process. Orthogonal to the theoretical concepts of software verification, we work on simplifying the use of SMT solvers, which are the basic foundation of several verification approaches. By introducing a common API layer written in Java with bindings towards several distinct SMT solvers, we make it more convenient for the engineer of a verification tool to interact with back-end solvers and even switch between those provide different features and strengths.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: software analysis, software verification, block-abstraction memoization, violation witness, CPAchecker, JavaSMT
• Themengebiete: 500 Naturwissenschaften und Mathematik > 510 Mathematik
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 3. November 2021
• 1. Bericht­erstatter:in: Beyer, Dirk