Refinement-based verification of sequential implementations of Stateflow charts - Alvaro Miyazawa; Ana Cavalcanti 001 (Refine@FM, 2011)

COMPASS tool vision for a system of systems Collaborative Development Environment. - Joey W. Coleman; Anders Kaels Malmos; Peter Gorm Larsen; Jan Peleska 001; Ralph Hains; Zoe Andrews; Richard John Payne; Simon Foster 001; Alvaro Miyazawa; Cristiano Bertolini; André Didier (SoSE, 2012)

Features of CML: A formal modelling language for Systems of Systems. - Jim Woodcock 001; Ana Cavalcanti 001; John S. Fitzgerald; Peter Gorm Larsen; Alvaro Miyazawa; Simon Perry (SoSE, 2012)

Refinement-oriented models of Stateflow charts. - Alvaro Miyazawa; Ana Cavalcanti 001 (Sci. Comput. Program., 2012)

Formal Models of SysML Blocks. - Alvaro Miyazawa; Lucas Lima 001; Ana Cavalcanti 001 (ICFEM, 2013)

Formal Refinement in SysML. - Alvaro Miyazawa; Ana Cavalcanti 001 (IFM, 2014)

Assurance Cases for Block-Configurable Software. - Richard Hawkins; Alvaro Miyazawa; Ana Cavalcanti 001; Tim Kelly; John Rowlands (SAFECOMP, 2014)

SysML contracts for systems of systems. - Jeremy W. Bryans; John S. Fitzgerald; Richard John Payne; Alvaro Miyazawa; Klaus E. Kristensen (SoSE, 2014)

An approach for managing semantic heterogeneity in Systems of Systems Engineering. - Simon Foster 001; Alvaro Miyazawa; Jim Woodcock 001; Ana Cavalcanti 001; John S. Fitzgerald; Peter Gorm Larsen (SoSE, 2014)

Refinement-based verification of implementations of Stateflow charts. - Alvaro Miyazawa; Ana Cavalcanti 001 (Formal Aspects Comput., 2014)

Refinement Strategies for Safety-Critical Java. - Alvaro Miyazawa; Ana Cavalcanti 001 (SBMF, 2015)

SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java. - Alvaro Miyazawa; Ana Cavalcanti 001 (Refine@FM, 2015)

From Formalised State Machines to Implementations of Robotic Controllers. - Wei Li 055; Alvaro Miyazawa; Pedro Ribeiro 002; Ana Cavalcanti 001; Jim Woodcock 001; Jon Timmis (DARS, 2016)

Java in the Safety-Critical Domain. - Ana Cavalcanti 001; Alvaro Miyazawa; Andy J. Wellings; Jim Woodcock 001; Shuai Zhao 004 (SETSS, 2016)

Sound Simulation and Co-simulation for Robotics. - Ana Cavalcanti 001; Alvaro Miyazawa; Richard John Payne; Jim Woodcock 001 (Present and Ulterior Software Engineering, 2017)

Modelling and Verification of Timed Robotic Controllers. - Pedro Ribeiro 002; Alvaro Miyazawa; Wei Li 055; Ana Cavalcanti 001; Jon Timmis (IFM, 2017)

Automatic property checking of robotic applications. - Alvaro Miyazawa; Pedro Ribeiro 002; Wei Li 055; Ana Cavalcanti 001; Jon Timmis (IROS, 2017)

An integrated semantics for reasoning about SysML design models using refinement. - Lucas Lima 001; Alvaro Miyazawa; Ana Cavalcanti 001; Márcio Cornélio; Juliano Iyoda; Augusto Sampaio 001; Ralph Hains; Adrian Larkham; Vaughan Lewis (Softw. Syst. Model., 2017)

Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. - Simon Foster 001; James Baxter 001; Ana Cavalcanti 001; Alvaro Miyazawa; Jim Woodcock 001 (FACS, 2018)

Modelling and Verification for Swarm Robotics. - Ana Cavalcanti 001; Alvaro Miyazawa; Augusto Sampaio 001; Wei Li 055; Pedro Ribeiro 002; Jon Timmis (IFM, 2018)

Verified simulation for robotics. - Ana Cavalcanti 001; Augusto Sampaio 001; Alvaro Miyazawa; Pedro Ribeiro 002; Madiel Conserva Filho; André Didier; Wei Li 055; Jon Timmis (Sci. Comput. Program., 2019)

SCJ-Circus: Specification and refinement of Safety-Critical Java programs. - Alvaro Miyazawa; Ana Cavalcanti 001; Andy J. Wellings (Sci. Comput. Program., 2019)

RoboChart: modelling and verification of the functional behaviour of robotic applications. - Alvaro Miyazawa; Pedro Ribeiro 002; Wei Li 055; Ana Cavalcanti 001; Jon Timmis; Jim Woodcock 001 (Softw. Syst. Model., 2019)

Model-Based Engineering for Robotics with RoboChart and RoboTool. - Ana Cavalcanti 001; Ziggy Attala; James Baxter 001; Alvaro Miyazawa; Pedro Ribeiro 002 (ICTAC Summmer School, 2021)

Architectural modelling for robotics: RoboArch and the CorteX example. - Will Barnett; Ana Cavalcanti 001; Alvaro Miyazawa (Frontiers Robotics AI, 2022)

Probabilistic modelling and verification using RoboChart and PRISM. - Kangfeng Ye; Ana Cavalcanti 001; Simon Foster 001; Alvaro Miyazawa; Jim Woodcock 001 (Softw. Syst. Model., 2022)

Bringing RoboStar and RT-Tester Together. - Ana Cavalcanti 001; Alvaro Miyazawa; Uwe Schulze; Jon Timmis (Applicable Formal Methods for Safe Industrial Products, 2023)

A Tour Through the Programming Choices: Semantics and Applications. - Pedro Ribeiro 002; Kangfeng Ye; Frank Zeyda; Alvaro Miyazawa (The Application of Formal Methods, 2024)

Software engineering for robotics. - Ana Cavalcanti 001; Alvaro Miyazawa; Jon Timmis (Robotics Auton. Syst., 2024)

Formal design, verification and implementation of robotic controller software via RoboChart and RoboTool. - Wei Li 055; Pedro Ribeiro 002; Alvaro Miyazawa; Richard Redpath; Ana Cavalcanti 001; Kieran Alden; Jim Woodcock 001; Jon Timmis (Auton. Robots, 2024)