Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Technology for Inferring Contracts from Code

Francesco Logozzo


Contracts are a simple yet very powerful form of specification. They consists of method preconditions and postconditions, of object invariants, and of assertions and loop invariants. Ideally, the programmer will annotate all of her code with contracts which are mechanically checked by some static analysis tool. In practice, programmers only write few contracts, mainly preconditions and some object invariants. The reason for that is that other contracts are “clear from the code”: Programmers do not like to repeat themselves.

As a consequence, any usable static verification tool should provide some form of contract inference.


Publication typeInproceedings
Published inProceedings of SigADA High Integrity Language Technology (HILT 2013)

Newer versions

Francesco Logozzo, Shuvendu Lahiri, Manuel Fahndrich, and Sam Blackshear. Verification Modulo Versions: Towards Usable Verification, ACM SIGPLAN, June 2014.

> Publications > Technology for Inferring Contracts from Code