-
Neurosymbolic C++ Verification in Rocq
May 12, 2026Neurosymbolic 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.
-
Verification of Templated Code in C++
Jan 17, 2026C++ 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.
-
Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic
Jan 17, 2026We present the current progress of specifying and verifying the NOVA microhypervisor at BlueRock Security. We carry out these tasks using the BRiCk C++ program logic and verification tools, building on top of the Iris framework for concurrent separation logics (CSLs), in Rocq. We found that the use of CSLs has enabled us to carry out highly modular specifications and verifications of even sophisticated, fine-grained concurrent algorithms in NOVA. We believe this is a significant step forward over other hypervisor verification projects that are either limited to single-threaded verification or are highly non-modular.
-
Recursive Mutexes in Separation Logic
Jan 17, 2026Mutexes (i.e., locks) are well understood in separation logic, and can be specified in terms of either protecting an invariant or atomically changing the state of the lock. In this abstract, we develop the same styles of specifications for _recursive_ mutexes, a common variant of mutexes in object-oriented languages like C++ and Java. A recursive mutex can be acquired any number of times by the same thread, and our specifications treat all acquires/releases uniformly, with clients only needing to determine whether they hold the mutex when accessing the lock invariant.
-
Modular, Full-System Verification
May 14, 2025We present an approach to specifying operating systems that is both highly modular and supports deriving various properties necessary to modern operating systems. The approach combines a machine semantics decomposed by privilege levels with a separation logic specification of the operating system API. We describe how the specification style enables natural proofs of robust safety in addition to deep behavioral refinements of user-mode applications running atop the OS. This approach enables simple and flexible concurrent specifications and unlocks new opportunities for whole-system verification.
- Read more
Gregory Malecha
Mullings on computer science and math: software verification, programming languages, compilers, and program analysis.