Bettering software development through HornSpec
2
MINS READ
Leading the way in innovation for over 55 years, we build greater futures for businesses across multiple industries and 55 countries.
Our expert, committed team put our shared beliefs into action – every day. Together, we combine innovation and collective knowledge to create the extraordinary.
We share news, insights, analysis and research – tailored to your unique interests – to help you deepen your knowledge and impact.
At TCS, we believe exceptional work begins with hiring, celebrating and nurturing the best people — from all walks of life.
Get access to a catalog of the latest news stories from across TCS. Discover our press releases, reports, and company announcements.
Sumanth Prabhu, Scientist, TCS Research
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.
Digital twin tech for sustainable food supply chain
Improving manufacturing process efficiency with unobtrusive sensing
Transforming Lives Through Service Design & Design for Change
AI workload migration to the cloud