Bettering software development through HornSpec
2
MINS READ
Navigate the AI era with confidence. TCS helps you turn AI into a strategic partner that empowers talent, reimagines processes, and accelerates business transformation.
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.
Deriving legal recommendations using NLP technique
2/4How AI and Sign Language Enable Inclusive Communication Experiences
3/4Driving Safe PQC Migration with Decision Intelligence Approach
4/4Digital Food Passport: Enhancing Transparency, Quality, Circularity