Modular Object-oriented Z Specifications. - Silvio Romero de Lemos Meira; Ana Cavalcanti 001 (Z User Workshop, 1990)

MooZ Case Studies. - Silvio Romero de Lemos Meira; Ana Cavalcanti 001 (Object Orientation in Z, 1992)

A refinement calculus for Z. - Ana Cavalcanti 001 (1997)

A Weakest Precondition Semantics for Z. - Ana Cavalcanti 001; Jim Woodcock 001 (Comput. J., 1998)

ZRC - A Refinement Calculus for Z. - Ana Cavalcanti 001; Jim Woodcock 001 (Formal Aspects Comput., 1998)

Procedures and Recursion in the Refinement Calculus. - Ana Cavalcanti 001; Augusto Sampaio 001; Jim Woodcock 001 (J. Braz. Comput. Soc., 1998)

A Weakest Precondition Semantics for an Object-Oriented Language of Refinement. - Ana Cavalcanti 001; David A. Naumann (World Congress on Formal Methods, 1999)

Cyber Rally: An experience of democratic use of the internet. - Geber L. Ramalho; Flávia A. Barros; Sérgio Cavalcante; Ana Cavalcanti 001; Manoel Lima; Silvio Romero de Lemos Meira; Hermano P. Moura; Alexandre M. L. de Vasconcelos (HCI (2), 1999)

An Inconsistency in Procedures, Parameters, and Substitution in the Refinement Calculus. - Ana Cavalcanti 001; Augusto Sampaio 001; Jim Woodcock 001 (Sci. Comput. Program., 1999)

Tactics of Refinement. - Marcel Oliveira; Ana Cavalcanti 001 (SBES, 2000)

A Weakest Precondition Semantics for Refinement of Object-Oriented Programs. - Ana Cavalcanti 001; David A. Naumann (IEEE Trans. Software Eng., 2000)

The Steam Boiler in a Unified Theory of Z and CSP. - Jim Woodcock 001; Ana Cavalcanti 001 (APSEC, 2001)

A Concurrent Language for Refinement. - Jim Woodcock 001; Ana Cavalcanti 001 (IWFM, 2001)

Forward Simulation for Data Refinement of Classes. - Ana Cavalcanti 001; David A. Naumann (FME, 2002)

Refinement in Circus. - Augusto Sampaio 001; Jim Woodcock 001; Ana Cavalcanti 001 (FME, 2002)

Refinement Algebra for Formal Bytecode Generation. - Adolfo Duran; Ana Cavalcanti 001; Augusto Sampaio 001 (ICFEM, 2002)

From CSP-OZ to Java with Processes. - Ana Cavalcanti 001; Augusto Sampaio 001 (IPDPS, 2002)

JACK: A Framework for Process Algebra Implementation in Java. - Leonardo Freitas; Augusto Sampaio 001; Ana Cavalcanti 001 (SBES, 2002)

The Semantics of Circus. - Jim Woodcock 001; Ana Cavalcanti 001 (ZB, 2002)

Refinement of actions in Circus. - Ana Cavalcanti 001; Augusto Sampaio 001; Jim Woodcock 001 (Refine, 2002)

Refactoring by Transformation. - Márcio Cornélio; Ana Cavalcanti 001; Augusto Sampaio 001 (Refine, 2002)

A Strategy for Compiling Classes, Inheritance, and Dynamic Binding. - Adolfo Duran; Ana Cavalcanti 001; Augusto Sampaio 001 (FME, 2003)

A Refinement Tool for Z. - Angela F. Freitas; Carla Nascimento; Ana Cavalcanti 001 (ICFEM, 2003)

Preface. - Ana Cavalcanti 001; Patrícia D. L. Machado (WMF, 2003)

A Refinement Strategy for Circus. - Ana Cavalcanti 001; Augusto Sampaio 001; Jim Woodcock 001 (Formal Aspects Comput., 2003)

ArcAngel: a Tactic Language for Refinement. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Formal Aspects Comput., 2003)

Predicate transformers in the semantics of Circus. - Ana Cavalcanti 001; Jim Woodcock 001 (IEE Proc. Softw., 2003)

From Circus to JCSP. - Marcel Oliveira; Ana Cavalcanti 001 (ICFEM, 2004)

A Framework for Specification and Validation of Real-Time Systems Using Circus Actions. - Adnan Sherif; Jifeng He 001; Ana Cavalcanti 001; Augusto Sampaio 001 (ICTAC, 2004)

A Tutorial Introduction to Designs in Unifying Theories of Programming. - Jim Woodcock 001; Ana Cavalcanti 001 (IFM, 2004)

Refinement: An overview. - Ana Cavalcanti 001; Augusto Sampaio 001; Jim Woodcock 001 (PSSE, 2004)

A Tutorial Introduction to CSP in Unifying Theories of Programming. - Ana Cavalcanti 001; Jim Woodcock 001 (PSSE, 2004)

Refine and Gabriel: Support for Refinement and Tactics. - Marcel Oliveira; Manuela Xavier; Ana Cavalcanti 001 (SEFM, 2004)

Refactoring Towards a Layered Architecture. - Márcio Cornélio; Ana Cavalcanti 001; Augusto Sampaio 001 (SBMF, 2004)

Algebraic reasoning for object-oriented programming. - Paulo Borba; Augusto Sampaio 001; Ana Cavalcanti 001; Márcio Cornélio (Sci. Comput. Program., 2004)

Control Law Diagrams in Circus. - Ana Cavalcanti 001; Phil Clayton; Colin O'Halloran (FM, 2005)

Operational Semantics for Model Checking Circus. - Jim Woodcock 001; Ana Cavalcanti 001; Leonardo Freitas (FM, 2005)

Angelic Nondeterminism and Unifying Theories of Programming. - Ana Cavalcanti 001; Jim Woodcock 001 (REFINE, 2005)

Mechanised Refinement of Procedures. - Manuela Xavier; Ana Cavalcanti 001 (SBMF, 2005)

Formal development of industrial-scale systems in Circus. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Innov. Syst. Softw. Eng., 2005)

Unifying classes and processes. - Ana Cavalcanti 001; Augusto Sampaio 001; Jim Woodcock 001 (Softw. Syst. Model., 2005)

Automatic Translation from Circus to Java. - Angela F. Freitas; Ana Cavalcanti 001 (FM, 2006)

Verification of Control Systems using Circus. - Ana Cavalcanti 001; Phil Clayton (ICECCS, 2006)

A Layered Behavioural Model of Platelets. - Steve A. Schneider; Helen Treharne; Ana Cavalcanti 001; Jim Woodcock 001 (ICECCS, 2006)

Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. - Leo Freitas; Ana Cavalcanti 001; Jim Woodcock 001 (ICFEM, 2006)

Pointers and Records in the Unifying Theories of Programming. - Ana Cavalcanti 001; Will Harwood; Jim Woodcock 001 (UTP, 2006)

Object-Orientation in the UTP. - Thiago L. V. L. Santos; Ana Cavalcanti 001; Augusto Sampaio 001 (UTP, 2006)

A Denotational Semantics for Circus. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Refine@ICFEM, 2006)

Type Checking Circus Specifications. - Manuela Xavier; Ana Cavalcanti 001; Augusto Sampaio 001 (SBMF, 2006)

Angelic nondeterminism in the unifying theories of programming. - Ana Cavalcanti 001; Jim Woodcock 001; Steve Dunne (Formal Aspects Comput., 2006)

State-rich model checking. - Leo Freitas; Jim Woodcock 001; Ana Cavalcanti 001 (Innov. Syst. Softw. Eng., 2006)

Testing for Refinement in CSP. - Ana Cavalcanti 001; Marie-Claude Gaudel (ICFEM, 2007)

Goal-Oriented Automatic Test Case Generators for MC/DC Compliancy. - Emine Gokce Aydal; Jim Woodcock 001; Ana Cavalcanti 001 (ICSOFT (SE), 2007)

A Theory of Pointers for the UTP. - Will Harwood; Ana Cavalcanti 001; Jim Woodcock 001 (ICTAC, 2008)

A Note on Traces Refinement and the conf Relation in the Unifying Theories of Programming. - Ana Cavalcanti 001; Marie-Claude Gaudel (UTP, 2008)

Encoding Circus Programs in ProofPowerZ. - Frank Zeyda; Ana Cavalcanti 001 (UTP, 2008)

Stateflow Diagrams in Circus. - Ana Cavalcanti 001 (SBMF, 2008)

ArcAngelC: a Refinement Tactic Language for Circus. - Marcel Oliveira; Ana Cavalcanti 001 (Refine@FM, 2008)

Guest Editorial. - Kamel Barkaoui; Manfred Broy; Ana Cavalcanti 001; Antonio Cerone (Formal Aspects Comput., 2008)

Mechanised Translation of Control Law Diagrams into Circus. - Frank Zeyda; Ana Cavalcanti 001 (IFM, 2009)

Supporting ArcAngel in ProofPower. - Frank Zeyda; Marcel Oliveira; Ana Cavalcanti 001 (REFINE@FMWeek, 2009)

A UTP semantics for Circus. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Formal Aspects Comput., 2009)

Communication Systems in ClawZ. - Michael Vernon; Frank Zeyda; Ana Cavalcanti 001 (ASM, 2010)

Automating Refinement of Circus Programs. - Frank Zeyda; Ana Cavalcanti 001 (SBMF, 2010)

Specification Coverage for Testing in Circus. - Ana Cavalcanti 001; Marie-Claude Gaudel (UTP, 2010)

An algebraic approach to the design of compilers for object-oriented languages. - Adolfo Duran; Ana Cavalcanti 001; Augusto Sampaio 001 (Formal Aspects Comput., 2010)

A process algebraic framework for specification and validation of real-time systems. - Adnan Sherif; Ana Cavalcanti 001; Jifeng He 001; Augusto Sampaio 001 (Formal Aspects Comput., 2010)

Special issue: 2nd World Congress on Formal Methods. - Ana Cavalcanti 001; Dennis Dams (Formal Methods Syst. Des., 2010)

Sound refactorings. - Márcio Cornélio; Ana Cavalcanti 001; Augusto Sampaio 001 (Sci. Comput. Program., 2010)

Programming Phase: Formal Methods. - Richard F. Paige; Jim Woodcock 001; Phillip J. Brooke; Ana Cavalcanti 001 (Encyclopedia of Software Engineering, 2010)

The Safety-Critical Java Memory Model: A Formal Account. - Ana Cavalcanti 001; Andy J. Wellings; Jim Woodcock 001 (FM, 2011)

The Safety-Critical Java Mission Model: A Formal Account. - Frank Zeyda; Ana Cavalcanti 001; Andy J. Wellings (ICFEM, 2011)

Safety-critical Java in Circus. - Ana Cavalcanti 001; Andy J. Wellings; Jim Woodcock 001; Kun Wei; Frank Zeyda (JTRES, 2011)

Conformance Relations for Distributed Testing Based on CSP. - Ana Cavalcanti 001; Marie-Claude Gaudel; Robert M. Hierons (ICTSS, 2011)

Testing for refinement in Circus. - Ana Cavalcanti 001; Marie-Claude Gaudel (Acta Informatica, 2011)

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

From control law diagrams to Ada via Circus. - Ana Cavalcanti 001; Phil Clayton; Colin O'Halloran (Formal Aspects Comput., 2011)

Editorial. - Ana Cavalcanti 001; Dennis Dams; Marie-Claude Gaudel (Formal Aspects Comput., 2011)

A tactic language for refinement of state-rich concurrent specifications. - Marcel Oliveira; Frank Zeyda; Ana Cavalcanti 001 (Sci. Comput. Program., 2011)

A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams. - Chris Marriott; Frank Zeyda; Ana Cavalcanti 001 (ABZ, 2012)

The cardiac pacemaker case study and its implementation in safety-critical Java and Ravenscar Ada. - Neeraj Kumar Singh 001; Andy J. Wellings; Ana Cavalcanti 001 (JTRES, 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)

Circus Time with Reactive Designs. - Kun Wei; Jim Woodcock 001; Ana Cavalcanti 001 (UTP, 2012)

Higher-Order UTP for a Theory of Methods. - Frank Zeyda; Ana Cavalcanti 001 (UTP, 2012)

Mechanised support for sound refinement tactics. - Frank Zeyda; Marcel Oliveira; Ana Cavalcanti 001 (Formal Aspects Comput., 2012)

Special issue: International Conference on Formal Engineering Methods - ICFEM 2009. - Ana Cavalcanti 001 (Sci. Comput. Program., 2012)

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

Mechanical reasoning about families of UTP theories. - Frank Zeyda; Ana Cavalcanti 001 (Sci. Comput. Program., 2012)

Special issue: International Colloquium on Theoretical Aspects of Computing - ICTAC 2010. - Ana Cavalcanti 001; David Déharbe (Theor. Comput. Sci., 2012)

Simulink Timed Models for Program Verification. - Ana Cavalcanti 001; Alexandre Mota 001; Jim Woodcock 001 (Theories of Programming and Formal Methods, 2013)

Testing with Inputs and Outputs in CSP. - Ana Cavalcanti 001; Robert M. Hierons (FASE, 2013)

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

Safety-critical Java level 2: motivations, example applications and issues. - Andy J. Wellings; Matt Luckcuck; Ana Cavalcanti 001 (JTRES, 2013)

Designs with Angelic Nondeterminism. - Pedro Ribeiro 002; Ana Cavalcanti 001 (TASE, 2013)

Refining SCJ Mission Specifications into Parallel Handler Designs - Frank Zeyda; Ana Cavalcanti 001 (Refine@IFM, 2013)

The Safety-Critical Java memory model formalised. - Ana Cavalcanti 001; Andy J. Wellings; Jim Woodcock 001 (Formal Aspects Comput., 2013)

Unifying theories in ProofPower-Z. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Formal Aspects Comput., 2013)

Safety-critical Java programs from Circus models. - Ana Cavalcanti 001; Frank Zeyda; Andy J. Wellings; Jim Woodcock 001; Kun Wei (Real Time Syst., 2013)

Data Flow Coverage for Circus-Based Testing. - Ana Cavalcanti 001; Marie-Claude Gaudel (FASE, 2014)

SCJ: Memory-Safety Checking without Annotations. - Chris Marriott; Ana Cavalcanti 001 (FM, 2014)

A Modular Theory of Object Orientation in Higher-Order UTP. - Frank Zeyda; Thiago L. V. L. Santos; Ana Cavalcanti 001; Augusto Sampaio 001 (FM, 2014)

A Formal Model for Natural-Language Timed Requirements of Reactive Systems. - Gustavo Carvalho; Ana Carvalho; Eduardo Rocha; Ana Cavalcanti 001; Augusto Sampaio 001 (ICFEM, 2014)

UTP Designs for Binary Multirelations. - Pedro Ribeiro 002; Ana Cavalcanti 001 (ICTAC, 2014)

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

Contracts in CML. - Jim Woodcock 001; Ana Cavalcanti 001; John S. Fitzgerald; Simon Foster 001; Peter Gorm Larsen (ISoLA (2), 2014)

Assurance Cases for Block-Configurable Software. - Richard Hawkins; Alvaro Miyazawa; Ana Cavalcanti 001; Tim Kelly; John Rowlands (SAFECOMP, 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)

Angelicism in the Theory of Reactive Processes. - Pedro Ribeiro 002; Ana Cavalcanti 001 (UTP, 2014)

Circus Models for Safety-Critical Java Programs. - Frank Zeyda; Lalkhumsanga Lalkhumsanga; Ana Cavalcanti 001; Andy J. Wellings (Comput. J., 2014)

Test-data generation for control coverage by proof. - Ana Cavalcanti 001; Steve King 001; Colin O'Halloran; Jim Woodcock 001 (Formal Aspects Comput., 2014)

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

CSP and Kripke Structures. - Ana Cavalcanti 001; Wen-ling Huang; Jan Peleska 001; Jim Woodcock 001 (ICTAC, 2015)

Safety-Critical Java Virtual Machine Services. - James Baxter 001; Ana Cavalcanti 001; Andy J. Wellings; Leo Freitas (JTRES, 2015)

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

Mobile CSP. - Jim Woodcock 001; Andy J. Wellings; Ana Cavalcanti 001 (SBMF, 2015)

NAT2TEST Tool: From Natural Language Requirements to Test Cases Based on CSP. - Gustavo Carvalho; Flávia A. Barros; Ana Carvalho; Ana Cavalcanti 001; Alexandre Mota 001; Augusto Sampaio 001 (SEFM, 2015)

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

Laws of mission-based programming. - Frank Zeyda; Ana Cavalcanti 001 (Formal Aspects Comput., 2015)

Test selection for traces refinement. - Ana Cavalcanti 001; Marie-Claude Gaudel (Theor. Comput. Sci., 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)

Checking SysML Models for Co-simulation. - Nuno Amálio; Richard John Payne; Ana Cavalcanti 001; Jim Woodcock 001 (ICFEM, 2016)

Local Livelock Analysis of Component-Based Models. - Madiel S. Conserva Filho; Marcel Vinícius Medeiros Oliveira; Augusto Sampaio 001; Ana Cavalcanti 001 (ICFEM, 2016)

Behavioural Models for FMI Co-simulations. - Ana Cavalcanti 001; Jim Woodcock 001; Nuno Amálio (ICTAC, 2016)

Modelling and Verifying a Priority Scheduler for an SCJ Runtime Environment. - Leo Freitas; James Baxter 001; Ana Cavalcanti 001; Andy J. Wellings (IFM, 2016)

A Formal Model of the Safety-Critical Java Level 2 Paradigm. - Matt Luckcuck; Ana Cavalcanti 001; Andy J. Wellings (IFM, 2016)

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

A Suspension-Trace Semantics for CSP. - Ana Cavalcanti 001; Robert M. Hierons; Sidney C. Nogueira; Augusto Sampaio 001 (TASE, 2016)

Towards a UTP Semantics for Modelica. - Simon Foster 001; Bernhard Thiele; Ana Cavalcanti 001; Jim Woodcock 001 (UTP, 2016)

A Stepwise Approach to Linking Theories. - Pedro Ribeiro 002; Ana Cavalcanti 001; Jim Woodcock 001 (UTP, 2016)

Modelling timed reactive systems from natural-language requirements. - Gustavo Carvalho; Ana Cavalcanti 001; Augusto Sampaio 001 (Formal Aspects Comput., 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)

Avoiding useless mutants. - Leonardo Fernandes; Márcio Ribeiro 001; Luiz Carvalho; Rohit Gheyi; Melina Mongiovi; André L. M. Santos; Ana Cavalcanti 001; Fabiano Cutigi Ferrari; José Carlos Maldonado (GPCE, 2017)

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

Algebraic Compilation of Safety-Critical Java Bytecode. - James Baxter 001; Ana Cavalcanti 001 (IFM, 2017)

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

Fault-Based Testing for Refinement in CSP. - Ana Cavalcanti 001; Adenilso da Silva Simão (ICTSS, 2017)

Formal Methods for Robotics: RoboChart, RoboSim, and More. - Ana Cavalcanti 001 (SBMF, 2017)

Local Analysis of Determinism for CSP. - Rodrigo Otoni; Ana Cavalcanti 001; Augusto Sampaio 001 (SBMF, 2017)

Formalising Cosimulation Models. - Frank Zeyda; Julien Ouy; Simon Foster 001; Ana Cavalcanti 001 (SEFM Workshops, 2017)

Safety-Critical Java: level 2 in practice. - Matt Luckcuck; Andy J. Wellings; Ana Cavalcanti 001 (Concurr. Comput. Pract. Exp., 2017)

Unifying Theories of Timed with Generalised Reactive Processes. - Simon Foster 001; Ana Cavalcanti 001; Jim Woodcock 001; Frank Zeyda (CoRR, 2017)

Formal mutation testing for Circus. - Alex D. B. Alberto; Ana Cavalcanti 001; Marie-Claude Gaudel; Adenilso Simão (Inf. Softw. Technol., 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)

Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. - Simon Foster 001; Kangfeng Ye; Ana Cavalcanti 001; Jim Woodcock 001 (RAMiCS, 2018)

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)

Compositional and local livelock analysis for CSP. - Madiel Conserva Filho; Marcel Vinícius Medeiros Oliveira; Augusto Sampaio 001; Ana Cavalcanti 001 (Inf. Process. Lett., 2018)

Unifying theories of time with generalised reactive processes. - Simon Foster 001; Ana Cavalcanti 001; Jim Woodcock 001; Frank Zeyda (Inf. Process. Lett., 2018)

Testing Robots Using CSP. - Ana Cavalcanti 001; James Baxter 001; Robert M. Hierons; Raluca Lefticaru (TAP@FM, 2019)

Probabilistic Semantics for RoboChart - A Weakest Completion Approach. - Jim Woodcock 001; Ana Cavalcanti 001; Simon Foster 001; Alexandre Mota 001; Kangfeng Ye (UTP, 2019)

Priorities in tock-CSP. - Pedro Ribeiro 002; James Baxter 001; Ana Cavalcanti 001 (CoRR, 2019)

Editorial. - Stefania Gnesi; Ana Cavalcanti 001; John S. Fitzgerald; Constance L. Heitmeyer (Formal Aspects Comput., 2019)

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)

Finite complete suites for CSP refinement testing. - Jan Peleska 001; Wen-ling Huang; Ana Cavalcanti 001 (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)

Fault-based refinement-testing for CSP. - Ana Cavalcanti 001; Adenilso Simão (Softw. Qual. J., 2019)

Angelic processes for CSP via the UTP. - Pedro Ribeiro 002; Ana Cavalcanti 001 (Theor. Comput. Sci., 2019)

Automated Verification of Reactive and Concurrent Programs by Calculation, supporting material. - Simon Foster 001; Kangfeng Ye; Ana Cavalcanti 001; Jim Woodcock 001 (Zenodo, 2019)

Modelling and Verification of Robotic Platforms for Simulation Using RoboStar Technology. - Ana Cavalcanti 001 (ABZ, 2020)

Editorial. - Ana Cavalcanti 001; Pedro Ribeiro 002 (Formal Aspects Comput., 2020)

Unifying semantic foundations for automated verification tools in Isabelle/UTP. - Simon Foster 001; James Baxter 001; Ana Cavalcanti 001; Jim Woodcock 001; Frank Zeyda (Sci. Comput. Program., 2020)

Unifying theories of reactive design contracts. - Simon Foster 001; Ana Cavalcanti 001; Samuel Canham; Jim Woodcock 001; Frank Zeyda (Theor. Comput. Sci., 2020)

Inputs and Outputs in CSP: A Model and a Testing Theory. - Ana Cavalcanti 001; Robert M. Hierons; Sidney C. Nogueira (ACM Trans. Comput. Log., 2020)

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)

Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata. - Abdulrazaq Abba; Ana Cavalcanti 001; Jeremy Jacob (SBMF, 2021)

RoboWorld: Where Can My Robot Work? - Ana Cavalcanti 001; James Baxter 001; Gustavo Carvalho (SEFM, 2021)

Transforming RoboSim Models into UPPAAL. - Mingzhuo Zhang; Dehui Du; Augusto Sampaio 001; Ana Cavalcanti 001; Madiel Conserva Filho; Menghan Zhang (TASE, 2021)

Editorial. - Erik P. de Vink; Ana Cavalcanti 001 (Formal Aspects Comput., 2021)

Automated verification of reactive and concurrent programs by calculation. - Simon Foster 001; Kangfeng Ye; Ana Cavalcanti 001; Jim Woodcock 001 (J. Log. Algebraic Methods Program., 2021)

RoboCert: Property Specification in Robotics. - Matt Windsor; Ana Cavalcanti 001 (ICFEM, 2022)

RoboSimVer: A Tool for RoboSim Modeling and Analysis. - Dehui Du; Ana Cavalcanti 001; Jihui Nie (ASE, 2022)

Sound reasoning in tock-CSP. - James Baxter 001; Pedro Ribeiro 002; Ana Cavalcanti 001 (Acta Informatica, 2022)

Correction to: Sound reasoning in tock-CSP. - James Baxter 001; Pedro Ribeiro 002; Ana Cavalcanti 001 (Acta Informatica, 2022)

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

From Pluralistic Normative Principles to Autonomous-Agent Rules. - Beverley A. Townsend; Colin Paterson; T. T. Arvind; Gabriel Nemirovsky; Radu Calinescu; Ana Cavalcanti 001; Ibrahim Habli; Alan Thomas (Minds Mach., 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)

UTP, Circus, and Isabelle. - Jim Woodcock 001; Ana Cavalcanti 001; Simon Foster 001; Marcel Oliveira; Augusto Sampaio 001; Frank Zeyda (Theories of Programming and Formal Methods, 2023)

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

Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment. - Mustafa Adam; Kangfeng Ye; David A. Anisi; Ana Cavalcanti 001; Jim Woodcock 001; Robert Morris (CASE, 2023)

Specification and Validation of Normative Rules for Autonomous Agents. - Sinem Getir Yaman; Charlie Burholt; Maddie Jones; Radu Calinescu; Ana Cavalcanti 001 (FASE, 2023)

Challenges in testing of cyclic systems. - Ana Cavalcanti 001; Robert M. Hierons (ICECCS, 2023)

Modelling and Verifying Robotic Software that Uses Neural Networks. - Ziggy Attala; Ana Cavalcanti 001; Jim Woodcock 001 (ICTAC, 2023)

Towards a Formal Framework for Normative Requirements Elicitation. - Nick Feng; Lina Marsso; Sinem Getir Yaman; Beverley A. Townsend; Ana Cavalcanti 001; Radu Calinescu; Marsha Chechik (ASE, 2023)

Trustworthy Autonomous Systems Through Verifiability. - Mohammad Reza Mousavi 001; Ana Cavalcanti 001; Michael Fisher 001; Louise A. Dennis; Robert M. Hierons; Bilal Y. Kaddouh; Effie Lai-Chong Law; Robert C. Richardson; Jan Oliver Ringert; Ivan Tyukin; Jim Woodcock 001 (Computer, 2023)

Testing using CSP Models: Time, Inputs, and Outputs. - James Baxter 001; Ana Cavalcanti 001; Maciej Gazda; Robert M. Hierons (ACM Trans. Comput. Log., 2023)

RoboWorld: Verification of Robotic Systems with Environment in the Loop. - James Baxter 001; Gustavo Carvalho; Ana Cavalcanti 001; Francisco Rodrigues Júnior (Formal Aspects Comput., 2023)

Safety assurance of autonomous agricultural robots: from offline model-checking to runtime verification. - Mustafa Adam; Elias E. Hartmark; Tage Andersen; David A. Anisi; Ana Cavalcanti 001 (CASE, 2024)

Analyzing and Debugging Normative Requirements via Satisfiability Checking. - Nick Feng; Lina Marsso; Sinem Getir Yaman; Yesugen Baatartogtokh; Reem Ayad; Victória Oldemburgo de Mello; Beverley A. Townsend; Isobel Standen; Ioannis Stefanakos; Calum Imrie; Genaína Nunes Rodrigues; Ana Cavalcanti 001; et al. (ICSE, 2024)

Trustworthy ROS Software Architecture for Autonomous Drones Missions: From RoboChart Modelling to ROS Implementation. - Nabil Shaukat; Shival Dubey; Bilal Y. Kaddouh; Andy Blight; Lenka Mudrich; Pedro Ribeiro 002; Hugo Araújo; Rob Richardson; Louise Abigail Dennis; Ana Lucia Caneca Cavalcanti; Mohammad Reza Mousavi 001 (MESA, 2024)

Normative Requirements Operationalization with Large Language Models. - Nick Feng; Lina Marsso; Sinem Getir Yaman; Isobel Standen; Yesugen Baatartogtokh; Reem Ayad; Victória Oldemburgo de Mello; Beverley A. Townsend; Hanne Bartels; Ana Cavalcanti 001; Radu Calinescu; Marsha Chechik (RE, 2024)

Laws of Timed State Machines. - Ana Cavalcanti 001; Madiel Conserva Filho; Pedro Ribeiro 002; Augusto Sampaio 001 (Comput. J., 2024)

Model Checking and Verification of Synchronisation Properties of Cobot Welding. - Yvonne Murray; Henrik Nordlie; David A. Anisi; Pedro Ribeiro 002; Ana Cavalcanti 001 (FMAS@iFM, 2024)

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

Robotic safe adaptation in unprecedented situations: the RoboSAPIENS project. - Peter Gorm Larsen; Shaukat Ali 001; Roland Behrens; Ana Cavalcanti 001; Cláudio Gomes 001; Guoyuan Li; Paul De Meulenaere; Mikkel Labori Olsen; Nikolaos Passalis; Thomas Peyrucain; Jesús Tapia; Anastasios Tefas; et al. (Res. Dir. Cyber Phys. Syst., 2024)

Toolkit for specification, validation and verification of social, legal, ethical, empathetic and cultural requirements for autonomous agents. - Sinem Getir Yaman; Pedro Ribeiro 002; Charlie Burholt; Maddie Jones; Ana Cavalcanti 001; Radu Calinescu (Sci. Comput. Program., 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)

Future Directions in Software Engineering for Autonomous Robots: An Agenda for Trustworthiness [Opinion]. - Davide Brugali; Ana Cavalcanti 001; Nico Hochgeschwender; Patrizio Pelliccione; Luciana Rebelo (IEEE Robotics Autom. Mag., 2024)

Scoping Software Engineering for AI: The TSE Perspective. - Sebastián Uchitel; Marsha Chechik; Massimiliano Di Penta; Bram Adams; Nazareno Aguirre; Gabriele Bavota; Domenico Bianculli; Kelly Blincoe; Ana Cavalcanti 001; Yvonne Dittrich; Filomena Ferrucci; Rashina Hoda; et al. (IEEE Trans. Software Eng., 2024)

Formal Architectural Patterns for Adaptive Robotic Software. - James Baxter 001; Bert Van Acker; Morten Haahr Kristensen; Thomas Wright; Ana Cavalcanti 001; Cláudio Gomes 001 (FASE, 2025)

RoboScene: Notation for Formal Verification of Human-Robot Interaction. - Holly Hendry; Ana Cavalcanti 001; Cade McCall; Mark Chattington (FASE, 2025)

Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software. - Ziggy Attala; Fang Yan 004; Simon Foster 001; Ana Cavalcanti 001; Jim Woodcock 001 (NFM, 2025)

Special Collection on Computer Science Education. - Luigia Petre; Ana Cavalcanti 001 (Formal Aspects Comput., 2025)

Specification, validation and verification of social, legal, ethical, empathetic and cultural requirements for autonomous agents. - Sinem Getir Yaman; Pedro Ribeiro 002; Ana Cavalcanti 001; Radu Calinescu; Colin Paterson; Beverley A. Townsend (J. Syst. Softw., 2025)

Software Engineering for Self-Adaptive Robotics: A Research Agenda. - Shaukat Ali 001; Ana Cavalcanti 001; Cláudio Ângelo Gonçalves Gomes; Peter Gorm Larsen; Hassan Sartaj; Anastasios Tefas; Jim Woodcock 001; Houxiang Zhang (CoRR, 2025)