Tagged “templates”

• Neurosymbolic C++ Verification in Rocq

  May 12, 2026

  Neurosymbolic capabilities have revolutionized the entire software development process, from requirements engineering and code development to testing and maintenence. In this talk, we will present our work integrating agentic techniques into the Brick C++ verification platform. Our approach combines algorithmic reasoning techniques, e.g. concurrent separation logic with sophisticated automation, proof search strategies, etc., with higher-level insights and probabilistic inference provided by LLMs. Our experience demonstrates that combining these technologies enables scalable reasoning for real-world programs.

  rocq c++ program verification separation logic brick templates skylabs-ai

• Verification of Templated Code in C++

  Jan 17, 2026

  C++ templates are used pervasively and a major blocker for applying verification to real code bases. We present an approach to verifying templated code that avoids enlarging the trusted computing base of the C++ semantics. Our approach uses a shallowly embedded logic that enables reasoning about unresolved symbols as hygienic macros. We have applied our approach to verify several small function templates and used their proofs to derive proofs for concrete instantiations of these functions.

  rocq c++ program verification separation logic brick templates skylabs-ai