CC(X): Semantic Combination of Congruence Closure with Solvable Theories. - Sylvain Conchon; Evelyne Contejean; Johannes Kanig; Stéphane Lescuyer (SMT@CAV, 2007)

Faire bonne figure avec MLPOST. - Romain Bardou; Jean-Christophe Filliâtre; Johannes Kanig; Stéphane Lescuyer (Stud. Inform. Univ., 2009)

Hi-Lite - Verification by Contract. - Johannes Kanig; Jérôme Guitton; Yannick Moy (Softwaretechnik-Trends, 2011)

Integration von Formaler Verifikation und Test. - Cyrille Comar; Johannes Kanig; Yannick Moy (Automotive - Safety & Security, 2012)

Reasoning with Triggers. - Claire Dross; Sylvain Conchon; Johannes Kanig; Andrei Paskevich (SMT@IJCAR, 2012)

Leading-edge ada verification technologies: combining testing and verification with GNATTest and GNATProve - the hi-lite project. - Johannes Kanig (HILT, 2012)

Hi-Lite: the convergence of compiler technology and program verification. - Johannes Kanig; Edmond Schonberg; Claire Dross (HILT, 2012)

Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification. - Johannes Kanig; Roderick Chapman; Cyrille Comar; Jérôme Guitton; Yannick Moy; Emyr Rees (TAP@STAF, 2014)

Bridging the Gap between Testing and Formal Verification in Ada Development. - Claude Marché; Johannes Kanig (ERCIM News, 2015)

Adding Decision Procedures to SMT Solvers Using Axioms with Triggers. - Claire Dross; Sylvain Conchon; Johannes Kanig; Andrei Paskevich (J. Autom. Reason., 2016)

Call Me Back, I Have a Type Invariant. - M. Anthony Aiello; Johannes Kanig; Taro Kurita (FM Workshops (1), 2019)

Recursive Data Structures in SPARK. - Claire Dross; Johannes Kanig (CAV (2), 2020)

Making Proofs of Floating-Point Programs Accessible to Regular Developers. - Claire Dross; Johannes Kanig (VSTTE, 2021)

Two-Way Collaboration Between Flow and Proof in SPARK. - Claire Dross; Joffrey Huguet; Johannes Kanig (VMCAI (1), 2025)