Parameterized software verification

Software model checking is one approach to ensuring computer system reliability, though its practical applications have been limited to either small "toy" systems or shallow correctness criteria (e.g., null-pointer dereference freedom). To cope with real systems with an unbounded amount of objects (e.g., processes, memory locations), and complex temporal specifications (e.g., trace serializability), analyses incorporating a thus far un-obtained balance of precision and scalability must be sought; indeed the usual abstractions used in existing tools (e.g., SLAM, BLAST) do not suffice. Here we seek to achieve the balance by using software abstractions that precisely model implementation details for a small number of representative software objects. We perform precise propositional reasoning between few representative objects involved in each system interaction to discharge quantified first-order candidate invariants in the deductive verification framework. These abstractions enable the first ever automatic proofs of program properties such as reference counting memory safety for virtual memory and file systems, and strict serializability for transactional memory managers, for an arbitrary number of processes and memory locations.