Skip to main content
Skip to footer
We're taking you to another TCS website now.

A technique finding maximal and non-vacuous specifications with the key component being an effective non-vacuous specifications synthesis algorithm. The approach is implemented in a tool—Horn Spec, taking as input systems of constrained Horn clauses.

By Sumanth Prabhu, Kumar Madhukar
Conference name- Programing Language Design and Implementation

Error: unable to play the video

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.


Connect with us to transform your workplace

*Required field
*Enter valid First Name
First Name
*Required field
*Enter valid Last Name
Last Name
*Required field
*Email syntax error
*Please use your business email.
*Required field
*Enter valid company name
Company Name
What's your challenge

Thank you for your interest

We will shortly connect.

Click here to submit another form.