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.
We are a digital transformation and technology partner of choice for industry-leading organizations worldwide.
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.
Safeguarding Organizations Against Financial Mismanagement and Fraud
Pushing the boundaries of edge computing
Future of Payments: From Money Movement to Value Exchange
Beyond the advantages and benefits of low-code no-code platforms