Scalable and Accurate SMT-based Model Checking of Data Flow Systems

: Model checking is a form of formal verification that can be used to check certain correctness properties of hardware or software systems mostly automatically. This project's overall objective was to improve the effectiveness and usefulness of model checking for embedded reactive software, the sort of software typically used in avionics. In particular, it sought to extend the scalability of model checking to systems with a very large or infinite state space, improve its accuracy, and develop modular model checking methods for infinite-state systems.! The project achieved its objectives by developing techniques based on automated reasoning engines called SMT solvers, which work with more powerful logics than propositional logic, the logic of choice in traditional model checking. These techniques were implemented in a automated model checker called Kind. Experimental results with Kind show that the new techniques provide superior scalability and precision. The tool has been adopted by several research groups from academia, government and industry. An internal reimplementation of Kind is now used regularly at a major avionics company.