5 papers
RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
Andrei Kozyrev, Nikita Khramov, Denis Lochmelis +3
This work studies the applicability of automatic AI agent optimization methods to real-world agents in formal verification settings, focusing on automated theorem proving in Rocq a…
Are Agents Probabilistic Automata? A Trace-Based, Memory-Constrained Theory of Agentic AI
Roham Koohestani, Ziyou Li, Anton Podkopaev +1
This paper studies standard controller architectures for agentic AI and derives automata-theoretic models of their interaction behavior via trace semantics and abstraction. We mode…
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
Andrei Kozyrev, Nikita Khramov, Gleb Solovev +1
Interactive Theorem Proving was repeatedly shown to be fruitful when combined with Generative Artificial Intelligence. This paper assesses multiple approaches to Rocq generation an…
LitmusKt: Concurrency Stress Testing for Kotlin
Denis Lochmelis, Evgenii Moiseenko, Yaroslav Golubev +1
We present LitmusKt - the first tool for litmus testing concurrent programs in Kotlin. The tool's novelty also lies in the fact that Kotlin is a multiplatform language, i.e., it co…
Can LLMs Enable Verification in Mainstream Programming?
Aleksandr Shefer, Igor Engel, Stanislav Alekseev +3
Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models i…