Unexpected behaviour in software can lead to catastrophic failures, especially in safety critical 
industries like healthcare, aviation and robotics. They guarantee that software will behave as expected 
can be given by formal verification and such a guarantee is invaluable, but can be challenging to automate 
it. For instance, when software is developed incrementally, there can be functions whose implementations 
are unavailable. It is essential for program. Verification to find specifications for such functions. This 
is an addition to finding adequate inductive invariants for complex control. Our paper, which has received 
the Distinguished Paper Award at ACM PLDI. 2021 conference, proposes a new technique that ensures that 
the software, which is developed incrementally, will work as it should without any unexpected behavior or 
technique. Finds maximal specifications as well as invariants. The specification being maximal allow for 
as many implementations or functions. As possible. This makes incremental development of correct software 
easier. This work was done in collaboration with Professor Grigory Fedyukovich from Florida State 
University and Professor Deepak D'souza from Indian Institute of Science. The main contribution of our 
paper is a new specification synthesis algorithm. It operates in an iterative loop, alternating between 
two models, specification and invariant Finder and maximality checker. The specifications and invariants 
are found using forward and backward reasoning. This generated solutions are passed to the maximality checker. 
This module lazily weakens the solution using counter examples. The algorithm loops between these two 
modules until a maximal specification is found. We are experimentally demonstrated our algorithms 
effectiveness efficiency. And the quality of specification generated on a range of standard benchmarks.