Model-Checking CSP-Z. - Alexandre Mota 001; Augusto Sampaio 001 (FASE, 1998)

Model-Checking Processes with States: An Industrial Case Study. - Alexandre Mota 001; Augusto Sampaio 001 (SBES, 1998)

Model-checking CSP-Z: strategy, tool support and industrial application. - Alexandre Mota 001; Augusto Sampaio 001 (Sci. Comput. Program., 2001)

Mechanical Abstraction of CSPZ Processes. - Alexandre Mota 001; Paulo Borba; Augusto Sampaio 001 (FME, 2002)

Class and Capsule Refinement in UML for Real Time. - Augusto Sampaio 001; Alexandre Mota 001; Rodrigo Ramos (WMF, 2003)

Efficient CSPZ Data Abstraction. - Adalberto Farias; Alexandre Mota 001; Augusto Sampaio 001 (IFM, 2004)

Preface. - Alexandre Mota 001; Arnaldo V. Moura (SBMF, 2004)

A Semantics for UML-RT Active Classes via Mapping into Circus. - Rodrigo Ramos; Augusto Sampaio 001; Alexandre Mota 001 (FMOODS, 2005)

Integrating UML and Formal Methods. - Rafael Magalhães Borges; Alexandre Cabral Mota (SBMF, 2005)

Towards Property Oriented Testing. - Patrícia D. L. Machado; Daniel A. Silva; Alexandre Mota 001 (SBMF, 2005)

Transformation Laws for UML-RT. - Rodrigo Ramos; Augusto Sampaio 001; Alexandre Mota 001 (FMOODS, 2006)

Viewing CSP Specifications with UML-RT Diagrams. - Patrícia Ferreira; Augusto Sampaio 001; Alexandre Mota 001 (SBMF, 2006)

Using Refinement Checking as System Testing. - Cristiano Bertolini; Alexandre Mota 001 (CIbSE, 2008)

Unifying Models of Test Cases and Requirements. - Clélio Feitosa; Glaucia Peres; Alexandre Mota 001 (CIbSE, 2008)

Guided Test Generation from CSP Models. - Sidney C. Nogueira; Augusto Sampaio 001; Alexandre Mota 001 (ICTAC, 2008)

Framework composition conformance via refinement checking. - Rodrigo Ramos; Augusto Sampaio 001; Alexandre Mota 001 (SAC, 2008)

Checking Z Data Refinements Using Traces Refinement. - André Didier; Adalberto Farias; Alexandre Mota 001 (SBMF, 2008)

Compositional Abstraction of CSPZ Processes. - Adalberto Farias; Alexandre Cabral Mota; Augusto Sampaio 001 (J. Braz. Comput. Soc., 2008)

Systematic Development of Trustworthy Component Systems. - Rodrigo Ramos; Augusto Sampaio 001; Alexandre Mota 001 (FM, 2009)

Compositional Verification of Input-Output Conformance via CSP Refinement Checking. - Augusto Sampaio 001; Sidney C. Nogueira; Alexandre Mota 001 (ICFEM, 2009)

An Empirical Evaluation of Automated Black Box Testing Techniques for Crashing GUIs. - Cristiano Bertolini; Glaucia Peres; Marcelo d'Amorim; Alexandre Mota 001 (ICST, 2009)

A Mechanized Strategy for Safe Abstraction of CSP Specifications. - Adriana Damasceno; Adalberto Farias; Alexandre Mota 001 (SBMF, 2009)

Formalisation and Analysis of Objects as CSP Processes. - Renata Kaufman; Augusto Sampaio 001; Alexandre Mota 001 (SBMF, 2009)

Using Probabilistic Model Checking to Evaluate GUI Testing Techniques. - Cristiano Bertolini; Alexandre Mota 001 (SEFM, 2009)

An Aspect-based Approach for Concurrent Programming using CSP Features. - José Elias Araújo; Henrique Rebêlo; Ricardo Massa Ferreira Lima; Alexandre Mota 001; Fernando Castor; Tiago Lima; Juliana Lucena; Filipe Lima (ICSOFT (2), 2010)

A Framework for GUI Testing Based on Use Case Design. - Cristiano Bertolini; Alexandre Mota 001 (ICST Workshops, 2010)

GUI Testing Techniques Evaluation by Designed Experiments. - Cristiano Bertolini; Alexandre Mota 001; Eduardo Aranha; Cristiano Ferraz (ICST, 2010)

Systematic Model-Based Safety Assessment Via Probabilistic Model Checking. - Adriano Gomes; Alexandre Mota 001; Augusto Sampaio 001; Felipe A. S. Ferri; Julio Buzzi (ISoLA (1), 2010)

Calibrating Probabilistic GUI Testing Models Based on Experiments and Survival Analysis. - Cristiano Bertolini; Alexandre Mota 001; Eduardo Aranha (ISSRE, 2010)

Evolving a Safe System Design Iteratively. - Alexandre Mota 001; Joabe Jesus; Adriano Gomes; Felipe A. S. Ferri; Edson H. Watanabe (SAFECOMP, 2010)

The contract enforcement aspect pattern. - Henrique Rebêlo; Ricardo M. F. Lima; Uirá Kulesza; Roberta Coelho; Alexandre Mota 001; Márcio Ribeiro 001; José Elias Araújo (SugarLoafPLoP, 2010)

Usando CSP, RSL e o Modelo PopOrg na Especificação Formal de Organizações de SMAs. - Raquel de Miranda Barbosa; Antônio Carlos da Rocha Costa; Patrícia Cabral de Azevedo Restelli Tedesco; Alexandre Cabral Mota (RITA, 2010)

Conformance notions for the coordination of interaction components. - Rodrigo Ramos; Augusto Sampaio 001; Alexandre Mota 001 (Sci. Comput. Program., 2010)

An annotation-based approach for JCSP concurrent programming: a quantitative study. - José Elias Araújo; Henrique Rebêlo; Ricardo Massa Ferreira Lima; Alexandre Mota 001; Uirá Kulesza; Cláudio Sant'Anna (MISS@AOSD, 2011)

Towards a more straightforward and more expressive metamodel for SDW modeling. - Paulo S. Ruiz Del Aguila; Robson do Nascimento Fidalgo; Alexandre Mota 001 (DOLAP, 2011)

On the interplay of exception handling and design by contract: an aspect-oriented recovery approach. - Henrique Rebêlo; Roberta Coelho; Ricardo M. F. Lima; Gary T. Leavens; Marieke Huisman; Alexandre Mota 001; Fernando Castor (FTfJP@ECOOP, 2011)

Architectural Verification of Control Systems Using CSP. - Joabe Jesus; Alexandre Mota 001; Augusto Sampaio 001; Luiz Grijo (ICFEM, 2011)

Assessing the Impact of Aspects on Design By Contract Effort: A Quantitative Study. - Henrique Rebêlo; Ricardo Massa Ferreira Lima; Uirá Kulesza; Cláudio Sant'Anna; Roberta Coelho; Alexandre Mota 001; Márcio Ribeiro 001; César A. L. de Oliveira (SEKE, 2011)

Introducing concurrency in sequential Java via laws. - Rafael M. Duarte; Alexandre Mota 001; Augusto Sampaio 001 (Inf. Process. Lett., 2011)

A Process Algebra Based Strategy for Generating Test Vectors from SCR Specifications. - Gustavo Carvalho; Diogo Falcão; Alexandre Mota 001; Augusto Sampaio 001 (SBMF, 2012)

Identifying Hardware Failures Systematically. - André Didier; Alexandre Mota 001 (SBMF, 2012)

Enforcing Contracts for Aspect-oriented programs with Annotations, Pointcuts and Advice. - Henrique Rebêlo; Ricardo Massa Ferreira Lima; Alexandre Mota 001; César A. L. de Oliveira; Márcio Ribeiro 001 (SEKE, 2012)

Checking Contracts for AOP using XPIDRs. - Henrique Rebêlo; Ricardo Massa Ferreira Lima; Alexandre Mota 001; César A. L. de Oliveira; Márcio Ribeiro 001 (SEKE, 2012)

Constructive model-based analysis for safety assessment. - Adriano Gomes; Alexandre Mota 001; Augusto Sampaio 001; Felipe A. S. Ferri; Edson H. Watanabe (Int. J. Softw. Tools Technol. Transf., 2012)

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

A CSP Timed Input-Output Relation and a Strategy for Mechanised Conformance Verification. - Gustavo Carvalho; Augusto Sampaio 001; Alexandre Mota 001 (ICFEM, 2013)

Creating GUI-based DSL formal tools. - Robson Silva; Alexandre Mota 001; Rodrigo Rizzi Starr (IRI, 2013)

Formal MDE-Based Tool Development. - Robson Silva; Alexandre Mota 001; Rodrigo Rizzi Starr (IRI (best papers), 2013)

Test case generation from natural language requirements based on SCR specifications. - Gustavo Carvalho; Diogo Falcão; Flávia A. Barros; Augusto Sampaio 001; Alexandre Mota 001; Leonardo Motta; Mark R. Blackburn (SAC, 2013)

Model-based development of fault tolerant systems of systems. - Zoe Andrews; Richard John Payne; Alexander B. Romanovsky; André Didier; Alexandre Mota 001 (SysCon, 2013)

Quantifying the effects of Aspectual Decompositions on Design by Contract Modularization: a Maintenance Study. - Henrique Rebêlo; Ricardo Massa Ferreira Lima; Uirá Kulesza; Márcio Ribeiro 001; Yuanfang Cai; Roberta Coelho; Cláudio Sant'Anna; Alexandre Mota 001 (Int. J. Softw. Eng. Knowl. Eng., 2013)

Optimizing generated aspect-oriented assertion checking code for JML using program transformations: An empirical study. - Henrique Rebêlo; Ricardo Massa Ferreira Lima; Gary T. Leavens; Márcio Cornélio; Alexandre Mota 001; César A. L. de Oliveira (Sci. Comput. Program., 2013)

Rapid Prototyping of a Semantically Well Founded Circus Model Checker. - Alexandre Mota 001; Adalberto Farias; André Didier; Jim Woodcock 001 (SEFM, 2014)

Test generation from state based use case models. - Sidney C. Nogueira; Augusto Sampaio 001; Alexandre Mota 001 (Formal Aspects Comput., 2014)

NAT2TESTSCR: Test case generation from natural language requirements based on SCR specifications. - Gustavo Carvalho; Diogo Falcão; Flávia de Almeida Barros; Augusto Sampaio 001; Alexandre Mota 001; Leonardo Motta; Mark R. Blackburn (Sci. Comput. Program., 2014)

Sound and mechanised compositional verification of input-output conformance. - Augusto Sampaio 001; Sidney C. Nogueira; Alexandre Mota 001; Yoshinao Isobe (Softw. Test. Verification Reliab., 2014)

A Lattice-Based Representation of Temporal Failures. - André Luis Ribeiro Didier; Alexandre Mota 001 (IRI, 2015)

Verifying Transformations of Java Programs Using Alloy. - Tarciana Dias da Silva; Augusto Sampaio 001; Alexandre Mota 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)

Model checking CML: tool development and industrial applications. - Alexandre Mota 001; Adalberto Farias; Jim Woodcock 001; Peter Gorm Larsen (Formal Aspects Comput., 2015)

Automatic Selection of Test Cases for Regression Testing. - Cláudio Magalhães; Flávia A. Barros; Alexandre Mota 001; Eliot Maia (SAST, 2016)

Model Checking Requirements. - Sérgio Barza; Gustavo Carvalho; Juliano Iyoda; Augusto Sampaio 001; Alexandre Mota 001; Flávia de Almeida Barros (SBMF, 2016)

An Approach for Verifying Educational Robots. - Sidney C. Nogueira; Taciana Pontual Falcão; Alexandre Mota 001; Emanuel Oliveira; Itamar Moraes; Iverson Pereira (SBMF, 2016)

Automatically Finding Hidden Industrial Criteria used in Test Selection. - Cláudio Magalhães; Alexandre Mota 001; Eliot Maia (SEKE, 2016)

Rigorous development of component-based systems using component metadata and patterns. - Marcel Vinícius Medeiros Oliveira; Pedro Antonino; Rodrigo Ramos; Augusto Sampaio 001; Alexandre Cabral Mota; A. W. Roscoe 001 (Formal Aspects Comput., 2016)

Program synthesis by model finding. - Alexandre Mota 001; Juliano Iyoda; Heitor Maranhão (Inf. Process. Lett., 2016)

An algebra of temporal faults. - André Didier; Alexandre Mota 001 (Inf. Syst. Frontiers, 2016)

Probabilistic Analysis Applied to Cleaning Robots. - Rafael Pereira de Araujo; Alexandre Cabral Mota; Sidney de Carvalho Nogueira (IRI, 2017)

Feasibility of using Source Code Changes on the Selection of Text-based Regression Test Cases. - Joelson Araújo; Jaedson Araújo; Cláudio Magalhães; João Andrade; Alexandre Mota 001 (SAST, 2017)

Evaluating an Automatic Text-based Test Case Selection using a Non-Instrumented Code Coverage Analysis. - Cláudio Magalhães; João Andrade; Lucas Perrusi; Alexandre Mota 001 (SAST, 2017)

SPt: A Text Mining Process to Extract Relevant Areas from SW Documents to Exploratory Tests. - Cloves Lima; Ivan Santos; Flávia A. Barros; Alexandre Mota 001 (BRACIS, 2018)

Analysing RoboChart with Probabilities. - Madiel S. Conserva Filho; R. Marinho; Alexandre Mota 001; Jim Woodcock 001 (SBMF, 2018)

The Pragmatic Dimension of Formal Methods: Towards Building a Sound Synthesiser. - Alexandre Mota 001 (SBMF, 2018)

Aiding exploratory testing with pruned GUI models. - Jacinto F. S. Reis; Alexandre Mota 001 (Inf. Process. Lett., 2018)

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

Combining model finder and genetic programming into a general purpose automatic program synthesizer. - Alexandre R. S. Correia; Juliano Iyoda; Alexandre Mota 001 (Inf. Process. Lett., 2020)

HSP: A hybrid selection and prioritisation of regression test cases based on information retrieval and code coverage applied on an industrial case study. - Cláudio Magalhães; João Andrade; Lucas Perrusi; Alexandre Mota 001; Flávia A. Barros; Eliot Maia (J. Syst. Softw., 2020)

A family of multi-concept program synthesisers in Alloy⁎. - Alexandre R. S. Correia; Juliano Iyoda; Alexandre Mota 001 (Sci. Comput. Program., 2021)

UI Test case prioritization on an industrial setting: A search for the best criteria. - Cláudio Magalhães; Alexandre Mota 001; Luis Momente (Softw. Qual. J., 2021)

The effect of distance metrics in a general purpose synthesizer: An empirical study on integer domain imperative programs. - Alexandre R. S. Correia; Juliano Manabu Iyoda; Alexandre Cabral Mota (Softw. Pract. Exp., 2022)

Assessor Models with a Reject Option for Soccer Result Prediction. - Daniel C. Da Costa; Ricardo B. C. Prudêncio; Alexandre Mota 001 (ICMLA, 2023)

Machine Learning Techniques for Escaped Defect Analysis in Software Testing. - Lidia Perside Gomes Nascimento; Ricardo Bastos Cavalcante Prudêncio; Alexandre Cabral Mota; Audir de Araujo Paiva Filho; Pedro Henrique Alves Cruz; Daniel Cardoso Coelho Alves de Oliveira; Pedro Roncoli Sarmet Moreira (SAST, 2023)

Formally Verifying a Real World Smart Contract. - Alexandre Mota 001; Fei Yang; Cristiano Teixeira (CoRR, 2023)

The effect of distance metrics in a general purpose synthesizer of imperative programs: A second empirical study using enlarged search spaces. - Alexandre R. S. Correia; Juliano Manabu Iyoda; Alexandre Cabral Mota (Softw. Pract. Exp., 2024)

Improving Android app exploratory testing with UI test cases using code change analysis. - Jacinto F. S. Reis; Alexandre Mota 001 (Innov. Syst. Softw. Eng., 2025)