49 citations · 71 across the 14 of their papers we have counts for
14 papers · 1 filter
Formal Verification of Access Control Model for My Health Record System
Victor Rivera
My Health Record system is the Australian Government's digital health record system that holds My Health Record. My Health Record is a secure online health record containing consum…
Size Matters: Microservices Research and Applications
Manuel Mazzara, Antonio Bucchiarone, Nicola Dragoni +1
In this chapter we offer an overview of microservices providing the introductory information that a reader should know before continuing reading this book. We introduce the idea of…
AutoFrame: Automatic Frame Inference for Object-Oriented Languages
Victor Rivera, Bertrand Meyer
Automatic program verification has made tremendous strides, but is not yet for the masses. How do we make it less painful? This article addresses one of the obstacles: the need to…
AutoAlias: Automatic Variable-Precision Alias Analysis for Object-Oriented Programs
Victor Rivera, Bertrand Meyer
The aliasing question (can two reference expressions point, during an execution, to the same object?) is both one of the most critical in practice, for applications ranging from co…
Model Checking in multiplayer games development
Ruslan Rezin, Ilya Afanasyev, Manuel Mazzara +1
Multiplayer computer games play a big role in the ever-growing entertainment industry. Being competitive in this industry means releasing the best possible software, and reliabilit…
Teaching Programming and Design-by-Contract
Daniel de Carvalho, Rasheed Hussain, Adil Khan +7
This paper summarizes the experience of teaching an introductory course to programming by using a correctness by construction approach at Innopolis University, Russian Federation.…
Domain Objects and Microservices for Systems Development: a roadmap
Kizilov Mikhail, Antonio Bucchiarone, Manuel Mazzara +2
This paper discusses a roadmap to investigate Domain Objects being an adequate formalism to capture the peculiarity of microservice architecture, and to support Software developmen…
Microservices Science and Engineering
Manuel Mazzara, Kevin Khanda, Ruslan Mustafin +3
In this paper we offer an overview on the topic of Microservices Science and Engineering (MSE) and we provide a collection of bibliographic references and links relevant to underst…
Translating Event-B machines to Eiffel programs
Victor Rivera, JooYoung Lee, Manuel Mazzara +1
Formal modelling languages play a key role in the development of software since they enable users to prove correctness of system properties. However, there is still not a clear und…
Initial steps towards assessing the usability of a verification tool
Mansur Khazeev, Victor Rivera, Manuel Mazzara +1
In this paper we report the experience of using AutoProof to statically verify a small object oriented program. We identified the problems that emerged by this activity and we clas…
Usability of AutoProof: a case study of software verification
Mansur Khazeev, Victor Rivera, Manuel Mazzara +1
Many verification tools come out of academic projects, whose natural constraints do not typically lead to a strong focus on usability. For widespread use, however, usability is ess…
Refinement types in Jolie
Alexander Tchitchigin, Larisa Safina, Manuel Mazzara +3
Jolie is the first language for microservices and it is currently dynamically type checked. This paper considers the opportunity to integrate dynamic and static type checking with…
Unifying Requirements and Code: an Example
Alexandr Naumchev, Bertrand Meyer, Victor Rivera
Requirements and code, in conventional software engineering wisdom, belong to entirely different worlds. Is it possible to unify these two worlds? A unified framework could help ma…
Code Generation for Event-B
Victor Rivera
Stepwise refinement and Design-by-Contract are two formal approaches for modelling systems. These approaches are widely used in the development of systems. Both approaches have (di…