Towards Verified Java Code Generation from Concurrent State Machines. - Dan Zhang 002; Dragan Bosnacki; Mark van den Brand; Luc Engelen; Cornelis Huizing; Ruurd Kuiper 001; Anton Wijs (AMT@MoDELS, 2014)

Towards Modular Verification of Threaded Concurrent Executable Code Generated from DSL Models. - Dragan Bosnacki; Mark van den Brand; Joost Gabriels; Bart Jacobs 002; Ruurd Kuiper 001; Sybren Roede; Anton Wijs; Dan Zhang 002 (FACS, 2015)

Verifying Atomicity Preservation and Deadlock Freedom of a Generic Shared Variable Mechanism Used in Model-To-Code Transformations. - Dan Zhang 002; Dragan Bosnacki; Mark van den Brand; Cornelis Huizing; Bart Jacobs 002; Ruurd Kuiper 001; Anton Wijs (MODELSWARD (Revised Selected Papers), 2016)

Verification of Atomicity Preservation in Model-to-Code Transformations using Generic Java Code. - Dan Zhang 002; Dragan Bosnacki; Mark van den Brand; Cornelis Huizing; Ruurd Kuiper 001; Bart Jacobs 002; Anton Wijs (MODELSWARD, 2016)

Dependency Safety for Java: Implementing Failboxes. - Dragan Bosnacki; Mark van den Brand; Philippe Denissen; Cornelis Huizing; Bart Jacobs 002; Ruurd Kuiper 001; Anton Wijs; Maciej Wilkowski; Dan Zhang 002 (PPPJ, 2016)

The SLCO Framework for Verified, Model-Driven Construction of Component Software. - Sander de Putter; Anton Wijs; Dan Zhang 002 (FACS, 2018)

Dependency safety for Java - Implementing and testing failboxes. - Dan Zhang 002; Dragan Bosnacki; Mark van den Brand; Cornelis Huizing; Bart Jacobs 002; Ruurd Kuiper 001; Anton Wijs (Sci. Comput. Program., 2019)