Java bytecode verification with dynamic structures. - Cinzia Bernardeschi; Luca Martini; Paolo Masci 001 (IASTED Conf. on Software Engineering and Applications, 2004)

A Space-Aware Bytecode Verifier for Java Cards. - Cinzia Bernardeschi; Giuseppe Lettieri; Luca Martini; Paolo Masci 001 (Bytecode@ETAPS, 2005)

VirtuS: a configurable layer for post-deployment adaptation of sensor network. - Paolo Corsini; Paolo Masci 001; Alessio Vecchio (ICWMC, 2006)

Configuration and tuning of sensor network applications through virtual sensors. - Paolo Corsini; Paolo Masci 001; Alessio Vecchio (PerCom Workshops, 2006)

Experiences with the TinyOS Communication Library. - Paolo Corsini; Paolo Masci 001; Alessio Vecchio (Wireless Information Systems, 2006)

Using Control Dependencies for Space-Aware Bytecode Verification. - Cinzia Bernardeschi; Giuseppe Lettieri; Luca Martini; Paolo Masci 001 (Comput. J., 2006)

Using postdomination to reduce space requirements of data flow analysis. - Cinzia Bernardeschi; Giuseppe Lettieri; Luca Martini; Paolo Masci 001 (Inf. Process. Lett., 2006)

Opportunistic computing for wireless sensor networks. - Marco Avvenuti; Paolo Corsini; Paolo Masci 001; Alessio Vecchio (MASS, 2007)

An application adaptation layer for wireless sensor networks. - Marco Avvenuti; Paolo Corsini; Paolo Masci 001; Alessio Vecchio (Pervasive Mob. Comput., 2007)

Early Prototyping of Wireless Sensor Network Algorithms in PVS. - Cinzia Bernardeschi; Paolo Masci 001; Holger Pfeifer (SAFECOMP, 2008)

Services for fault-tolerant conflict resolution in air traffic management. - Paolo Masci 001; Henrique Moniz; Alessandra Tedeschi (SERENE, 2008)

Decomposing bytecode verification by abstract interpretation. - Cinzia Bernardeschi; Nicoletta De Francesco; Giuseppe Lettieri; Luca Martini; Paolo Masci 001 (ACM Trans. Program. Lang. Syst., 2008)

Analysis of Wireless Sensor Network Protocols in Dynamic Scenarios. - Cinzia Bernardeschi; Paolo Masci 001; Holger Pfeifer (SSS, 2009)

Dependability Analysis of Diffusion Protocols in Wireless Networks with Heterogeneous Node Capabilities. - Paolo Masci 001; Silvano Chiaradonna; Felicita Di Giandomenico (EDCC, 2010)

Dependability Analysis and Verification for Connected Systems. - Felicita Di Giandomenico; Marta Z. Kwiatkowska; Marco Martinucci; Paolo Masci 001; Hongyang Qu 001 (ISoLA (2), 2010)

Metrics for QoS analysis in dynamic, evolving and heterogeneous connected systems. - Antinisca Di Marco; Antonia Bertolino; Felicita Di Giandomenico; Paolo Masci 001; Antonino Sabetta (WODA, 2010)

Comparing Actual Practice and User Manuals: A Case Study Based on Programmable Infusion Pumps. - Ann Blandford; Abigail Cauchi; Paul Curzon; Parisa Eslambolchilar; Dominic Furniss; Andy Gimblett; Huayi Huang; Paul Lee; Yunqiu Li; Paolo Masci 001; Patrick Oladimeji; Atish Rajkomar; et al. (EICS4Med, 2011)

Towards Dependable Number Entry for Medical Devices. - Abigail Cauchi; Paul Curzon; Parisa Eslambolchilar; Andy Gimblett; Huayi Huang; Paul Lee; Yunqiu Li; Paolo Masci 001; Patrick Oladimeji; Rimvydas Ruksenas; Harold Thimbleby (EICS4Med, 2011)

Towards a formal framework for reasoning about the resilience of dynamic interactive systems. - Paolo Masci 001; Paul Curzon; Huayi Huang; Rimvydas Ruksenas; Ann Blandford; Dominic Furniss; Atish Rajkomar (EWDC, 2011)

Automated Refinement of Dependability Analysis through Monitoring in Dynamically Connected Systems. - Antonia Bertolino; Antonello Calabrò; Felicita Di Giandomenico; Marco Martinucci; Paolo Masci 001 (ISADS, 2011)

Towards Automated Dependability Analysis of Dynamically Connected Systems. - Paolo Masci 001; Marco Martinucci; Felicita Di Giandomenico (ISADS, 2011)

On Enabling Dependability Assurance in Heterogeneous Networks through Automated Model-Based Analysis. - Paolo Masci 001; Nicola Nostro; Felicita Di Giandomenico (SERENE, 2011)

Checking User-Centred Design Principles in Distributed Cognition Models: A Case Study in the Healthcare Domain. - Paolo Masci 001; Paul Curzon (USAB, 2011)

Modelling Distributed Cognition Systems in PVS. - Paolo Masci 001; Paul Curzon; Ann Blandford; Dominic Furniss (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

On formalising interactive number entry on infusion pumps. - Paolo Masci 001; Rimvydas Ruksenas; Patrick Oladimeji; Abigail Cauchi; Andy Gimblett; Karen Yunqiu Li; Paul Curzon; Harold W. Thimbleby (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Safer "5-key" number entry user interfaces using differential formal analysis. - Abigail Cauchi; Andy Gimblett; Harold W. Thimbleby; Paul Curzon; Paolo Masci 001 (BCS HCI, 2012)

Using PVS to Investigate Incidents through the Lens of Distributed Cognition. - Paolo Masci 001; Huayi Huang; Paul Curzon; Michael D. Harrison (NASA Formal Methods, 2012)

Supporting Field Investigators with PVS: A Case Study in the Healthcare Domain. - Paolo Masci 001; Dominic Furniss; Paul Curzon; Michael D. Harrison; Ann Blandford (SERENE, 2012)

JCSI: A tool for checking secure information flow in Java Card applications. - Marco Avvenuti; Cinzia Bernardeschi; Nicoletta De Francesco; Paolo Masci 001 (J. Syst. Softw., 2012)

MediCHI: safer interaction in medical devices. - Karen Yunqiu Li; Sharon Xianghua Ding; Zhanxun Dong; Liping Qin; Paolo Masci 001; Chris J. Vincent; Harold W. Thimbleby; Abigail Cauchi; Alexis Lewis; Sisy Baixi Xing; Shouqian Sun; Eric Liu; et al. (CHI Extended Abstracts, 2013)

Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. - Paolo Masci 001; Anaheed Ayoub; Paul Curzon; Michael D. Harrison; Insup Lee 001; Harold W. Thimbleby (EICS, 2013)

Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS. - Paolo Masci 001; Anaheed Ayoub; Paul Curzon; Insup Lee 001; Oleg Sokolsky; Harold W. Thimbleby (SAFECOMP, 2013)

Automated theorem proving for the systematic analysis of an infusion pump. - Michael D. Harrison; Paolo Masci 001; José Creissac Campos; Paul Curzon (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

PVSio-web: a tool for rapid prototyping device user interfaces in PVS. - Patrick Oladimeji; Paolo Masci 001; Paul Curzon; Harold W. Thimbleby (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. - Rimvydas Ruksenas; Paolo Masci 001; Michael D. Harrison; Paul Curzon (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Formal Verification of Medical Device User Interfaces Using PVS. - Paolo Masci 001; Yi Zhang 051; Paul L. Jones; Paul Curzon; Harold W. Thimbleby (FASE, 2014)

Demonstrating that Medical Devices Satisfy User Related Safety Requirements. - Michael D. Harrison; Paolo Masci 001; José Creissac Campos; Paul Curzon (FHIES/SEHC, 2014)

Using PVSio-web to Demonstrate Software Issues in Medical User Interfaces. - Paolo Masci 001; Patrick Oladimeji; Paul Curzon; Harold Thimbleby (FHIES/SEHC, 2014)

A Generic User Interface Architecture for Analyzing Use Hazards in Infusion Pump Software. - Paolo Masci 001; Yi Zhang 051; Paul L. Jones; Harold Thimbleby; Paul Curzon (MCPS, 2014)

Combining PVSio with Stateflow. - Paolo Masci 001; Yi Zhang 051; Paul L. Jones; Patrick Oladimeji; Enrico D'Urso; Cinzia Bernardeschi; Paul Curzon; Harold Thimbleby (NASA Formal Methods, 2014)

Automated synthesis of dependable mediators for heterogeneous interoperable systems. - Felicita Di Giandomenico; Massimiliano Leone Itria; Paolo Masci 001; Nicola Nostro (Reliab. Eng. Syst. Saf., 2014)

PVSio-web 2.0: Joining PVS to HCI. - Paolo Masci 001; Patrick Oladimeji; Yi Zhang 051; Paul L. Jones; Paul Curzon; Harold W. Thimbleby (CAV (1), 2015)

Reusing models and properties in the analysis of similar interactive devices. - Michael D. Harrison; José Creissac Campos; Paolo Masci 001 (Innov. Syst. Softw. Eng., 2015)

Using PVS to support the analysis of distributed cognition systems. - Paolo Masci 001; Paul Curzon; Dominic Furniss; Ann Blandford (Innov. Syst. Softw. Eng., 2015)

The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. - Paolo Masci 001; Rimvydas Ruksenas; Patrick Oladimeji; Abigail Cauchi; Andy Gimblett; Karen Yunqiu Li; Paul Curzon; Harold W. Thimbleby (Innov. Syst. Softw. Eng., 2015)

Exploring medical device design and use through layers of Distributed Cognition: How a glucometer is coupled with its context. - Dominic Furniss; Paolo Masci 001; Paul Curzon; Astrid Mayer; Ann Blandford (J. Biomed. Informatics, 2015)

Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. - Rimvydas Ruksenas; Paolo Masci 001; Paul Curzon (From Action Systems to Distributed Systems, 2016)

Modeling communication network requirements for an integrated clinical environment in the Prototype Verification System. - Cinzia Bernardeschi; Andrea Domenici; Paolo Masci 001 (ISCC, 2016)

Evaluation of Formal IDEs for Human-Machine Interface Design and Analysis: The Case of CIRCUS and PVSio-web. - Camille Fayollas; Célia Martinie; Philippe A. Palanque; Paolo Masci 001; Michael D. Harrison; José Creissac Campos; Saulo Rodrigues e Silva (F-IDE@FM, 2016)

PVSio-web: mathematically based tool support for the design of interactive and interoperable medical systems. - Paolo Masci 001; Patrick Oladimeji; Piergiuseppe Mallozzi; Paul Curzon; Harold Thimbleby (EAI Endorsed Trans. Collab. Comput., 2016)

Templates as heuristics for proving properties of medical devices. - Michael D. Harrison; José Creissac Campos; Paolo Masci 001; Paul Curzon (EAI Endorsed Trans. Creative Technol., 2016)

Issues in number entry user interface styles: Recommendations for mitigation. - Harold Thimbleby; Patrick Oladimeji; Paolo Masci 001; Paul Curzon (EAI Endorsed Trans. Creative Technol., 2016)

IWC Special Issue in Human Factors and Interaction Design for Critical Systems. - Huawei Tu; Paolo Masci 001; Chris J. Vincent; Karen Yunqiu Li; Harold Thimbleby (Interact. Comput., 2016)

Towards a Formalization of System Requirements for an Integrated Clinical Environment. - Cinzia Bernardeschi; Andrea Domenici; Paolo Masci 001 (EAI Endorsed Trans. Self Adapt. Syst., 2016)

The Specification and Analysis of Use Properties of a Nuclear Control System. - Michael D. Harrison; Paolo M. Masci; José Creissac Campos; Paul Curzon (Handbook of Formal Methods in Human-Computer Interaction, 2017)

Safety Analysis of Software Components of a Dialysis Machine Using Model Checking. - Michael D. Harrison; Michael J. Drinnan; José Creissac Campos; Paolo Masci 001; Leo Freitas; Costanzo di Maria; Michael Whitaker (FACS, 2017)

TOM: A Model-Based GUI Testing Framework. - Miguel Pinto; Marcelo Gonçalves; Paolo Masci 001; José Creissac Campos (FACS, 2017)

A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices. - Paolo Masci 001; Yi Zhang 051; Paul L. Jones; José Creissac Campos (SEFM, 2017)

Co-simulation of Semi-autonomous Systems: The Line Follower Robot Case Study. - Maurizio Palmieri; Cinzia Bernardeschi; Paolo Masci 001 (SEFM Workshops, 2017)

Verification of User Interface Software: The Example of Use-Related Safety Requirements and Programmable Medical Devices. - Michael D. Harrison; Paolo Masci 001; José Creissac Campos; Paul Curzon (IEEE Trans. Hum. Mach. Syst., 2017)

Modeling and Analysis of Human Memory Load in Multitasking Scenarios: Late-Breaking Results. - Giovanna Broccia; Paolo Masci 001; Paolo Milazzo (EICS, 2018)

Data Leakage in Java Applets with Exception Mechanism. - Cinzia Bernardeschi; Paolo Masci 001; Antonella Santone (ITASEC, 2018)

Formal Modelling as a Component of User Centred Design. - Michael D. Harrison; Paolo Masci 001; José Creissac Campos (STAF Workshops, 2018)

A Flexible Framework for FMI-Based Co-Simulation of Human-Centred Cyber-Physical Systems. - Maurizio Palmieri; Cinzia Bernardeschi; Paolo Masci 001 (STAF Workshops, 2018)

Integrating User Design and Formal Models within PVSio-Web. - Nathaniel Watson; Steve Reeves; Paolo Masci 001 (F-IDE@FLoC, 2018)

A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems. - Cinzia Bernardeschi; Andrea Domenici; Paolo Masci 001 (IEEE Trans. Software Eng., 2018)

Experiences with Streamlining Formal Methods Tools. - Paolo Masci 001 (FM Workshops (1), 2019)

An Integrated Development Environment for the Prototype Verification System. - Paolo Masci 001; César A. Muñoz (F-IDE@FM, 2019)

Formal techniques in the safety analysis of software components of a new dialysis machine. - Michael D. Harrison; Leo Freitas; Michael J. Drinnan; José Creissac Campos; Paolo Masci 001; Costanzo di Maria; Michael Whitaker (Sci. Comput. Program., 2019)

The benefits of using interactive device simulations as training material for clinicians: an experience report with a contrast media injector used in CT. - Cinzia Bernardeschi; Paolo Masci 001; Davide Caramella; Ruggero Dell'Osso (SIGBED Rev., 2019)

A use error taxonomy for improving human-machine interface design in medical devices. - Carlos Silva 005; Paolo Masci 001; Yi Zhang 051; Paul L. Jones; José Creissac Campos (SIGBED Rev., 2019)

Verification Templates for the Analysis of User Interface Software Design. - Michael D. Harrison; Paolo Masci 001; José Creissac Campos (IEEE Trans. Software Eng., 2019)

Logic-Based Formalization of System Requirements for Integrated Clinical Environments. - Cinzia Bernardeschi; Andrea Domenici; Paolo Masci 001 (Automated Reasoning for Systems Biology and Medicine, 2019)

A Graphical Toolkit for the Validation of Requirements for Detect and Avoid Systems. - Paolo Masci 001; César A. Muñoz (TAP@STAF, 2020)

A framework for FMI-based co-simulation of human-machine interfaces. - Maurizio Palmieri; Cinzia Bernardeschi; Paolo Masci 001 (Softw. Syst. Model., 2020)

Supporting the Analysis of Safety Critical User Interfaces: An Exploration of Three Formal Tools. - José Creissac Campos; Camille Fayollas; Michael D. Harrison; Célia Martinie; Paolo Masci 001; Philippe A. Palanque (ACM Trans. Comput. Hum. Interact., 2020)

Proving Display Conformance and Action Consistency: The Example of an Integrated Clinical Environment. - Michael D. Harrison; Paolo Masci 001 (INTERACT (Workshops), 2021)

Control Rooms from a Human-Computer Interaction Perspective. - Tilo Mentler; Philippe A. Palanque; Michael D. Harrison; Kristof Van Laerhoven; Paolo Masci 001 (INTERACT (Workshops), 2021)

Balancing the formal and the informal in user-centred design. - Michael D. Harrison; Paolo Masci 001; José Creissac Campos (Interact. Comput., 2021)

Interpretation and Formalization of the Right-of-Way Rules. - Victor A. Carreño; Mariano M. Moscato; Paolo M. Masci; Aaron Dutle (FACS, 2022)

Proof Mate: An Interactive Proof Helper for PVS (Tool Paper). - Paolo Masci 001; Aaron Dutle (NFM, 2022)

Towards an implementation of differential dynamic logic in PVS. - J. Tanner Slagel; César A. Muñoz; Swee Balachandran; Mariano M. Moscato; Aaron Dutle; Paolo Masci 001; Lauren M. White (SOAP@PLDI, 2022)

Formal analysis of the application programming interface of the PVS verification system. - Paolo Masci 001 (J. Log. Algebraic Methods Program., 2022)

Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0. - Laura Titolo; Mariano M. Moscato; Marco A. Feliú; Paolo Masci 001; César A. Muñoz (FM (2), 2024)