Neurosymbolic C++ Verification in Rocq

Lennart Beringer, Jasper Haag, Rodolphe Lepigre, Gregory Malecha, Rayan Soban, Ehtesham Zahoor

HCSS'26 - 2026

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

Verification of Templated Code in C++

Gregory Malecha, David Swasey, Simon Hudon

RocqPL'26 - 2026

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

Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic

Hoang-Hai Dang, Gregory Malecha

RocqPL'26 - 2026

rocq c++ program verification separation logic brick concurrency nova hypervisor skylabs-ai bluerock-security

Recursive Mutexes in Separation Logic

Ke Du, William Mansky, Paolo G. Giarrusso, Gregory Malecha

RocqPL'26 - 2026

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

Modular, Full-System Verification

Gregory Malecha, Hoang-Hai Dang, Paolo G. Giarrusso, Simon Hudon, Jan-Oliver Kaiser, David Swasey

HotOS'25 - 2025

microkernel full-system c++ program verification separation logic brick concurrency

Towards an Axiomatic Basis for C++

Gregory Malecha, Abhishek Anand, and Gordon Stewart

Coq Workshop 2020 - 2020

rocq c++ program verification separation logic axiomatic semantics

Interaction Trees: Representing Recursive and Impure Programs in Coq

Li-yao Xai, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic

POPL'20 - 2020

rocq coinduction denotational semantics

Compositional Non-termination without Fuel

Gregory Malecha

NEPLS'18 - 2018

rocq coinduction denotational semantics

Predicate Monads

Edwin Westbrook and Gregory Malecha

CoqPL'17 - 2017

rocq monads verification logic

Modular Deductive Verification of Sampled-Data Systems

Daniel Ricketts and Gregory Malecha and Sorin Lerner

EMSOFT'16 - 2016

rocq veridrone cyber-physical

Towards Foundational Verification of Cyber-physical Systems

Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, Sorin Lerner

SoSCYPS'16 - 2016

rocq veridrone cyber-physical

Formal Verification of Stability Properties in Cyber-physical Systems

Matthew Chan, Daniel Ricketts, Sorin Lerner, Gregory Malecha

CoqPL'16 - 2016

cyber-physical systems veridrone stability

Extensible and Efficient Automation through Reflective Tactics

Gregory Malecha and Jesper Bengtson

ESOP'16 - 2016

rocq rtac computation reflection automation

Towards Verification of Hybrid Systems in a Foundational Proof Assistant

Daniel Ricketts, Gregory Malecha, Mario M. Alvarez, Vignesh Gowda and Sorin Lerner

MEMOCODE'15 - 2015

cyber-physical systems verification

Using Dependent Types and Tactics to Enable Semantic Optimization of Language-Integrated Queries

Gregory Malecha and Ryan Wisnesky

DBPL'15 - 2015

rocq refinment databases optimization

Extensible Proof Engineering in Intensional Type Theory

Gregory Malecha

PhD Dissertation - 2015

mirror-core rtac rocq computational reflection

Rtac: A Fully Reflective Tactic Language

Gregory Malecha and Jesper Bengston

CoqPL'15 - 2015

rtac rocq computational reflection automation

Automating Abstract Logics (a.k.a. Implementing Reflective Tactics)

Gregory Malecha, Jesper Bengston, and Adam Chlipala

Coq'14 - 2014

mirror-core rocq computational reflection automation talk

Compositional Computational Reflection

Gregory Malecha, Thomas Braibant, and Adam Chlipala

ITP'14 - 2014

mirror-core rocq computational reflection automation

MirrorShard: Proof by Computational Reflection with Verified Hints

Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, and Edward Yang

Tech Report - 2013

mirror-shard rocq computational reflection automation

Reflecting Modular Automation

Gregory Malecha

Talk @ INRIA - 2013

talk rocq mirror-shard computational reflection

Compiling Coq in Coq

Gregory Malecha

Talk @ INRIA - 2013

rocq compilation

Building Bedrock: Verifying a Program Verifier

Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, and Edward Yang

Coq'13 - 2012

mirror-shard rocq computational reflection automation

Mechanized Verification with Sharing

Gregory Malecha, Greg Morrisett

ICTAC'10 - 2010

rocq separation logic ynot

A More Precise Security Type System for Dynamic Security Tests

Gregory Malecha and Stephen Chong

PLAS'10 - 2010

information flow security

Toward a verified relational database management system

Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky

POPL'10 - 2010

ynot rocq b+ tree separation logic

Trace-based verification of imperative programs with I/O

Gregory Malecha and Greg Morrisett and Ryan Wisnesky

JSC'11 - 2010

ynot separation logic rocq verification

Effective interactive proofs for higher-order imperative programs

Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky

ICFP'09 - 2009

ynot separation logic rocq verification