@inproceedings{bib_Doub_2025, AUTHOR = {Garg, Mohit and TIFR, N Raja and Saraswat, Suneel and Singh, Abhishek Kr }, TITLE = {Double Auctions: Formalization and Automated Checkers}, BOOKTITLE = {Journal of Automated Reasoning}. YEAR = {2025}}

Double auctions are widely used in financial markets, such as those for stocks, derivatives, currencies, and commodities, to match demand and supply. Once all buyers and sellers have placed their trade requests, the exchange determines how these requests are to be matched. The two most common objectives for determining the matching are maximizing trade volume at a uniform price and maximizing trade volume through dynamic pricing. In this work, we present fully formalized matching algorithms for double auctions, along with their correctness proofs. We establish new uniqueness theorems, enabling automatic detection of violations in exchange systems by comparing their output to that of a verified program. All proofs are formalized in the Coq Proof Assistant; we extract verified OCaml and Haskell programs that could serve as a resource for exchanges and market regulators. We demonstrate the practical applicability of our work by running the verified program on real market data from an exchange to automatically check for violations in the exchange algorithm.

@inproceedings{bib_Deci_2024, AUTHOR = {Singh, Abhishek Kr and Lahav, Ori }, TITLE = {Decidable Verification under Localized Release-Acquire Concurrency}, BOOKTITLE = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems}. YEAR = {2024}}

State reachability for finite state concurrent programs running under Release-Acquire (RA) semantics is known to be undecidable, while under a weaker variant, called Weak-Release-Acquire (WRA), the problem is decidable. However, WRA allows many counterintuitive behaviors not allowed under RA, in which threads locally oscillate between observed values. We propose a strengthening of WRA in the form of a new memory model, which we call Localized Release-Acquire (LRA), that prunes these oscillatory behaviors. We provide semantics for LRA and show that verification under LRA is decidable by extending the potential-based technique used to prove decidability under WRA. The LRA model is still weaker than RA, and thus our results can be used to soundly verify programs under RA.

@inproceedings{bib_An_O_2023, AUTHOR = {Singh, Abhishek Kr and Lahav, Ori }, TITLE = {An Operational Approach to Library Abstraction under Relaxed Memory Concurrency}, BOOKTITLE = {Proceedings of Programming Languages}. YEAR = {2023}}

Concurrent data structures and synchronization mechanisms implemented by expert developers are indispensable for modular software development. In this paper, we address the fundamental problem of library abstraction under weak memory concurrency, and identify a general library correctness condition allowing clients of the library to reason about program behaviors using the specification code, which is often much simpler than the concrete implementation. We target (a fragment of) the RC11 memory model, and develop an equivalent operational presentation that exposes knowledge propagation between threads, and is sufficiently expressive to capture library behaviors as totally ordered operational execution traces. We further introduce novel access modes to the language that allow intricate specifications accounting for library internal synchronization that is not exposed to the client, as well as the library's demands on external synchronization by the client. We illustrate applications of our approach in several examples of different natures.

@inproceedings{bib_Veri_2021, AUTHOR = {Natarajan, Raja and Saraswat, Suneel and Singh, Abhishek Kr }, TITLE = {Verified Double Sided Auctions for Financial Markets}, BOOKTITLE = {Interactive Theorem Proving}. YEAR = {2021}}

Double sided auctions are widely used in financial markets to match demand and supply. Prior works on double sided auctions have focused primarily on single quantity trade requests. We extend various notions of double sided auctions to incorporate multiple quantity trade requests and provide fully formalized matching algorithms for double sided auctions with their correctness proofs. We establish new uniqueness theorems that enable automatic detection of violations in an exchange program by comparing its output with that of a verified program. All proofs are formalized in the Coq proof assistant without adding any axiom to the system. We extract verified OCaml and Haskell programs that can be used by the exchanges and the regulators of the financial markets. We demonstrate the practical applicability of our work by running the verified program on real market data from an exchange to automatically check for violations in the exchange algorithm.

@inproceedings{bib_Sepa_2016, AUTHOR = {Singh, Abhishek Kr and Natarajan, Raja }, TITLE = {Separation Logic to Meliorate Software Testing and Validation}, BOOKTITLE = {Trends in Software Testing}. YEAR = {2016}}

The ideal goal of any program logic is to develop logically correct programs without the need for predominant debugging. Separation logic is considered to be an effective program logic for proving programs that involve pointers. Reasoning with pointers becomes difficult especially due to the way they interfere with the modular style of program development. For instance, often there is aliasing arising due to several pointers to a given cell location. In such situations, any alteration to that cell in one of the program modules may affect the values of many syntactically unrelated expressions in other modules. In this chapter, we try to explore these difficulties through some simple examples and introduce the notion of separating conjunction as a tool to deal with it. We introduce separation logic as an extension of Hoare Logic using a programming language that has four pointer-manipulating commands. These commands perform the usual heap operations such as lookup, update, allocation and de-allocation. The new set of assertions and axioms of separation logic are presented in a semi-formal style. Examples are given to illustrate unique features of the new assertions and axioms. Finally, the chapter concludes with proofs of some real programs using the axioms of separation logic.