Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems
PRIN 2007 DIT-PRJ-10-028
Status NOT active project
DISI role Coordinator
Project type Research Project
Dimension National
Acquisition date 2008-09-01
Start date 2008-09-01
End date 2010-08-31
SAP code 40101443
Project details
Project astract Computer systems pervade more and more our everyday lives. We rely on complex programmable electronic systems to supervise critical functions of automobiles, airplanes and industrial sites, just to name a few. In these contexts, dependability of the underlying hardware and software components becomes of paramount importance. However, traditional verification techniques such as simulation and testing do not guarantee the absence of flaws, and thus impact severely on the reliability of the components it produces. Formal methods, by introducing formal rigour in the specification, design, and verification phases, yield the needed level of assurance. Nevertheless, the sheer size of industrial-scale software and hardware artifacts makes their manual application unfeasible. Automatic verification techniques are thus becoming key to the development of critical software and hardware applications. In this scenario Model Checking (MC) has emerged as the most successful automatic technique for the formal verification of finite-state systems like hardware circuits and communication protocols. MC has been successfully used to verify several industrial-strength hardware designs, including the IEEE Futurebus+ cache coherence protocol. Remarkably, the success of MC is due to a large extent to breakthroughs in automated reasoning for Boolean logic: OBDDs enabled model checkers to tackle industrial-strength problems; more recently, improvements in SAT solving led to the development of model checkers that can solve even larger problems. The development of MC techniques for software, RTL hardware designs and, more generally, for very-large or even infinite-state systems, is a more recent undertaking that calls for effective automated reasoning techniques, namely decision procedures in richer domains than Boolean logic such as theories of commonly-used data structures (e.g. arrays, lists, bit-vectors). This is an especially ambitious goal, as MC is generally undecidable for this class of systems. Yet, the development of novel MC techniques has shown that remarkable results are within reach: several serious bugs in device drivers of both the Windows and Linux operating systems were detected and fixed using software MC. However, the effectiveness of these techniques is currently limited to control intensive programs (like device drivers), and further work is needed to develop new MC methods capable of handling other, more mundane, classes of programs. A large number of model checkers and decision procedures for a variety of application domains has been put forward in the last decade. While this fact witnesses the liveness of the research area, the sheer number of available tools makes it very difficult to determine which tool is most suited for which problem class. This project will contribute to the development of a new generation of MC techniques for data-intensive software and industrial-scale hardware designs by developing:a new MC procedures based on the counterexample-driven abstraction refinement paradigm; a new MC procedures that exploit the modular structure of specifications; a new decision procedures for theories of commonly-used data structures such as arrays, lists, bit-vectors, and heap data structures; machine learning techniques for automated selection and tuning of the reasoning and verification tools so to optimise their performance and effectively relieve the user from the burden of extensive manual tuning; libraries of benchmark problems for the quantitative assessment of the effectiveness of the reasoning and verification techniques developed within the project; relationships between features of relevant problems and the performance of formal verification techniques, through controlled experimentation with several benchmarks and tools. The methodology employed in the project will be a combination of theoretical developments and empirical investigation. The theoretical pursuit will be to prove general properties (e.g. decidability or worst-case complexity) or limitations of the techniques developed within the project. The empirical investigation will aim at understanding properties and limitations of the developed techniques. The consortium has the right blend of expertise to meet the challenges of the project: UNIGE (project coordinator) has a long experience in the development of decision procedures and their application to verification. The unit has also a strong record in the coordination of both national and international research projects; UNINA has a strong background in abstract interpretation, software MC, module checking and automata; UNITN is the key contributor of MathSAT and NuSMV, state-of-the-art tools for satisfiability modulo theories and MC respectively; UNIVR has a strong expertise in automated theorem proving, decision procedures, satisfiability modulo theories and automated model building.<br/>
Fundings 35000 €