A Behavioral Synthesis Frontend to the Haste/TiDE Design Flow. - Sune Fallgaard Nielsen; Jens Sparsø; Jonas Braband Jensen; Johan Sebastian Rosenkilde Nielsen (ASYNC, 2009)

Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. - Jesper Bengtson; Jonas Braband Jensen; Filip Sieczkowski; Lars Birkedal (ITP, 2011)

Modular Verification of Linked Lists with Views via Separation Logic. - Jonas Braband Jensen; Lars Birkedal; Peter Sestoft (J. Object Technol., 2011)

Fictional Separation Logic. - Jonas Braband Jensen; Lars Birkedal (ESOP, 2012)

Charge! - A Framework for Higher-Order Separation Logic in Coq. - Jesper Bengtson; Jonas Braband Jensen; Lars Birkedal (ITP, 2012)

High-level separation logic for low-level code. - Jonas Braband Jensen; Nick Benton; Andrew Kennedy (POPL, 2013)

Coq: the world's best macro assembler? - Andrew Kennedy; Nick Benton; Jonas Braband Jensen; Pierre-Évariste Dagand (PPDP, 2013)