LtRules

Abstract

The need to manually specify temporal properties of software systems is a major barrier to wider adoption of software model checking, because the specification of software temporal properties is a difficult, time-consuming, and error-prone process. To address this problem, we propose to automatically extract software library usage rules, which are one type of temporal specifications. Our approach uses a model checker to check a set of software library usage rule candidates against known good programs using that library, and identifies valid rules based on model checking results. These valid rules can help programmers learn about common software library usage. They can also be used to check new programs using the same library. We have implemented our approach in an Eclipse plug-in named LtRules, which can extract software library usage rules from C programs using BLAST as the underlying model checker.