Skip to main content
Skip to footer

Author

Sumanth Prabhu, Scientist, TCS Research

Highlights

  • A new technique proposed to find maximal specifications and invariants.
  • The proposition is a new specification synthesis algorithm that operates in loop – an iterative algorithm. 
  • The approach is implemented in a tool—HornSpec—taking input systems of constrained Horn clauses.

My paper in 2 minutes

Specific synthesis with constrained Horn clauses 

 

Unexpected behavior in software can lead to catastrophic failure and loss, especially in safety-critical industries. Program verification gives a formal guarantee that a software will behave as expected. Such a guarantee is invaluable but challenging to do automatically. For instance, when a software is developed incrementally, there will be functions whose implementations are unavailable. It is essential for program verification to find specifications of such functions. This is in addition to finding adequate invariants for complex control-flow. 

This paper proposes a new technique that finds maximal specifications and invariants. The specifications being maximal allows for as many implementations of functions as possible. The main contribution of the paper is a new specification synthesis algorithm. It operates in an iterative algorithm, in loop, alternating between two modules--first, a specification and invariant finding module, and second, a maximality checking module. The approach is implemented in a tool called HornSpec, taking input systems of constrained Horn clauses. The paper has experimentally demonstrated the algorithm’s effectiveness, efficiency, and the quality of generated specifications on a range of standard benchmarks.