Permissive interfaces

A modular program analysis considers components independently and provides succinct summaries for each component, which can be used when checking the rest of the system. Consider a system comprising of two components, a library and a client. A temporal summary, or interface, of the library specifies legal sequences of library calls. The interface is safe if no call sequence violates the library's internal invariants; the interface is permissive if it contains every such sequence. Modular program analysis requires full interfaces, which are both safe and permissive: the client does not cause errors in the library if and only if it makes only sequences of library calls that are allowed by the full interface of the library. Previous interface-based methods have focused on safe interfaces, which may be too restrictive and thus reject good clients. We present an algorithm for automatically synthesizing software interfaces that are both safe and permissive. The algorithm generates inte...

• Type: Conference
• Year: 2005
• Where: SIGSOFT
• Authors: Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
• Keywords: Algorithm Generates Interfaces, Library Calls, Library Specifies, SIGSOFT 2005, Software Engineering