Program Synthesis and Non-Monotonic Reasoning - Kedar Namjoshi

Leading formal methods researcher Kedar Namjoshi (Distinguished Member of Technical Staff, Nokia Bell Labs) discusses his extended abstract “Program Synthesis And Non-monotonic Reasoning”.

This conversation explores why standard logical specifications, while well-suited for verification, can lead synthesis procedures to produce programs with unnecessary or undesirable actions, and how introducing minimality and preferences fundamentally changes the reasoning model required for synthesis.

Kedar shares the research motivations behind the work, tracing its roots to non-monotonic logic and his experience synthesizing real-world control programs, and reflects on how practical scenarios like IoT device coordination expose deep gaps between formal specifications and human expectations of reasonable system behavior.

In This Episode -

• Why logical specifications are ideal for verification but problematic for synthesis

• The notion of superfluous actions in synthesized programs

• An IoT case study - door locks and refrigerators

• How preference and minimality introduce non-monotonicity into synthesis

• Compact strategies and minimizing behaviors in reactive systems

• Checking minimality versus performing synthesis• Scaling synthesis to multi-agent systems (i.e., robotics)

• Automaton-based approach limitations and LLM-based synthesis

References -

• https://synt2025.github.io/

• https://link.springer.com/chapter/10.1007/978-3-030-99524-9_3

• https://en.wikipedia.org/wiki/Alonzo_Church

• https://dl.acm.org/doi/10.1145/3689624

• https://www.youtube.com/watch?v=H53JDxt_cbI

• https://www.youtube.com/watch?v=s6GKwRIQRf0

About the Paper -

“Program Synthesis And Non-monotonic Reasoning (Extended Abstract)”

Kedar S. NamjoshiPresented at SYNT 2025 Workshop

The paper shows that enforcing minimality in program synthesis breaks monotonic reasoning assumptions, reframing the avoidance of unnecessary actions as a problem of preference-based, non-monotonic reasoning.

https://drive.google.com/file/d/1btOZ52OLD_RuvYc8KIkEk0rLDBn0lBvR/view?usp=sharing

About the Guest -

Kedar Namjoshi is a Distinguished Member of Technical Staff at Nokia Bell Labs. His research spans formal methods, program synthesis, verification, distributed systems, and the design of correct-by-construction systems, with an emphasis on bridging theory and real-world applications.

https://kedar-namjoshi.github.io

Credits -

• Host & Music: Bryan Landers, Technical Staff, Ndea

• Editor: Alejandro Ramirez

• https://x.com/ndea

• https://x.com/bryanlanders

• https://ndea.com