Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems

DIT-PRJ-08-073

Status NOT active project
DISI role Partner
Project type Research Project
Dimension National
Acquisition date 2008-09-22
Start date 2008-09-22
End date 2010-09-21
SAP code 40101442

Project details

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

DISI Sub-project details

Fundings 35000 €
Manager Roberto Sebastiani