Bettering software development through HornSpec
2
MINS READ
At TCS, we don’t just help businesses transform. We help them become perpetually adaptive enterprises, built to evolve continuously and confidently in a world of constant change.
We deliver excellence and create value for customers and communities - everyday. With the best talent and the latest technology we help customers turn complexity into opportunities and create meaningful change.
Point of views, research, studies - on the latest themes - to help you expand your knowledge and be future ready.
At TCS, we believe exceptional work begins with hiring, celebrating and nurturing the best people — from all walks of life.
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.
Biodiversity: The Next Frontier for Business Growth
Automated Compliance: Driving Software-Defined Vehicle Forward
A robust architecture for real-time satellite sensing data
A Journey from Software Development to Visual Intelligence Research