2 papers
cs.PL2026
Agentic Separation Logic Specification Synthesis
Tarun Suresh, David Korczynski, Julien Vanegue
Specification synthesis, the task of automatically inferring formal specifications from program implementations and natural language, is important for refactoring, transpilation, o…
cs.PL2025
Non-Termination Proving: 100 Million LoC and Beyond
Julien Vanegue, Jules Villard, Peter O'Hearn +1
We report on our tool, Pulse Infinite, that uses proof techniques to show non-termination (divergence) in large programs. Pulse Infinite works compositionally and under-approximate…