C. Liu, E. Ye, and D.J. Richardson
Software verification, model checking, software library usage pattern
The need to manually specify temporal properties of software systems is a major barrier to wider adoption of software model checking. To address this problem, we propose to automatically extract software library usage patterns, i.e., one type of temporal specifications. Our approach uses a model checker to check a set of template-based pattern candidates against existing programs, and identifies valid patterns based on model checking results. We applied our approach to extract one valid pattern of the C standard library from 500 C programs in Sourceforge.net using BLAST, and used the extracted pattern to detect an error in an open source project.
Important Links:
Go Back
