Giving your co-programmer maximum leeway

Computer programs are ubiquitous, be it the browser you are using to read this or the operating system in which the browser is running. Programs may have errors that cause them to exhibit unexpected behaviours. To find errors before they affect users, programs are typically tested. Testing can never guarantee that a program is error-free, but such a guarantee is invaluable for programs used in safety-critical systems. A formal guarantee that a program will behave in expected ways can be achieved automatically by program verification.

In incremental software development, it is common to have to reason about programs with function calls to functions whose bodies are yet to be written. This is handled by finding a constraint on the input and output of the function and using it in place of the function call. Such a constraint is called a specification, and the process of finding a specification is called specification synthesis. To allow for as many implementations of the function as possible, the weakest possible specification is desirable. This is a challenge for programs with complex control flow such as loops and recursion, because along with a specification, one also needs to synthesize invariants for these control-flow structures.

In a recent paper titled “Specification Synthesis with Constrained Horn Clauses” which won a distinguished paper award at the ACM PLDI 2021 conference, Sumanth Prabhu S, Deepak D’Souza, and their collaborators propose a technique that, for the first time, not only finds maximally weak specifications, but also finds accompanying invariants for complex control flow. The technique handles programs represented as Constrained Horn Clauses. This makes it widely applicable as Constrained Horn Clauses are a general framework which can represent many other verification and synthesis problems such as safety games.

This research is a collaborative work between Sumanth Prabhu S (TCS Research and IISc), Grigory Fedyukovich (Florida State University), Kumar Madhukar (TCS Research, India) and Deepak D’Souza (IISc).

REFERENCE:

S. Prabhu, G. Fedyukovich, K. Madhukar, and D. D’Souza.

Specification Synthesis with Constrained Horn Clauses., To appear in Proc. ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), 2021.

https://doi.org/10.1145/3453483.3454104 [available after conference]

LAB WEBSITE:

https://www.csa.iisc.ac.in/~deepakd/