Integrating automated reasoning in model checking: towards push-button formal verification of large-scale and infinite-state systems - Design and integration of proof engines for program analysis

Since computer software is everywhere, the economic impact of software errors cannot be overestimated. The cost of errors could be significantly reduced by techniques that enable earlier and more effective identification and removal of defects. The importance of the problem demands to investigate fully automated techniques. The successes of model checking in hardware and protocol verification suggest to investigate software model checking. However, software model checking is considerably harder, because software involves infinite state systems. Complexity is attacked by abstraction: if a piece of software is too complex, an abstract version that is simpler than the original is analyzed. However, an error detected in the abstract model is not necessarily an error in the concrete program. In order to bridge this gap, model checking needs automated reasoning. The correspondence between an error in the model and an error in the concrete program is reduced to a satisfiability problem, whose proof can be used to refine the abstraction, if it turns out that a spurious error was detected. The thrust of this project is to define, design and implement efficient, scalable and expressive decision procedures for satisfiability.