Scalable Model Checking Using Compiler Analyses and the Alef SAT Solver

Our objective is to produce a commercial-grade model checking system that is scalable, end-to-end and highly usable. By scalable, we mean that the system will check larger software systems and answer more detailed queries than existing systems. By end-to-end, we mean that the system will automate the entire model-checking process from the point where the developer submits a query to the point where results are presented to the developer. By highly usable, we mean that the developer will not be required to learn any special-purpose modeling or specification languages in order to make full use of the system.