72 citations · 97 across the 10 of their papers we have counts for
12 papers
Model checking of hyperproperties for high-level relational models
Nuno Macedo, Hugo Pacheco
Many properties related to security or concurrency must be encoded as so-called hyperproperties, temporal properties that allow reasoning about multiple traces of a system. However…
Synthesizing Test Cases for Narrowing Specification Candidates
Alcino Cunha, Nuno Macedo
This paper proposes a technique to help choose the best formal specification candidate among a set of alternatives. Given a set of specifications, our technique generates a suite o…
Validating Formal Specifications with LLM-generated Test Cases
Alcino Cunha, Nuno Macedo
Validation is a central activity when developing formal specifications. Similarly to coding, a possible validation technique is to define upfront test cases or scenarios that a fut…
The High-Assurance ROS Framework
André Santos, Alcino Cunha, Nuno Macedo
This tool paper presents the High-Assurance ROS (HAROS) framework. HAROS is a framework for the analysis and quality improvement of robotics software developed using the popular Ro…
Simulation under Arbitrary Temporal Logic Constraints
Julien Brunel, David Chemouil, Alcino Cunha +1
Most model checkers provide a useful simulation mode, that allows users to explore the set of possible behaviours by interactively picking at each state which event to execute next…
ROSY: An elegant language to teach the pure reactive nature of robot programming
Hugo Pacheco, Nuno Macedo
Robotics is incredibly fun and is long recognized as a great way to teach programming, while drawing inspiring connections to other branches of engineering and science such as math…
Sharing and Learning Alloy on the Web
Nuno Macedo, Alcino Cunha, José Pereira +5
We present Alloy4Fun, a web application that enables online editing and sharing of Alloy models and instances, to be used mainly in an educational context. By introducing the notio…
Improving the Visualization of Alloy Instances
Rui Couto, José C. Campos, Nuno Macedo +1
Alloy is a lightweight formal specification language, supported by an IDE, which has proven well-suited for reasoning about software design in early development stages. The IDE pro…
Alloy meets TLA+: An exploratory study
Nuno Macedo, Alcino Cunha
Alloy and TLA+ are two formal specification languages that are increasingly popular due to their simplicity and flexibility, as well as the effectiveness of their companion model c…
A Feature-based Classification of Model Repair Approaches
Nuno Macedo, Tiago Jorge, Alcino Cunha
Consistency management, the ability to detect, diagnose and handle inconsistencies, is crucial during the development process in Model-driven Engineering (MDE). As the popularity a…
A Generic Scheme and Properties of Bidirectional Transformations
Hugo Pacheco, Nuno Macedo, Alcino Cunha +1
The recent rise of interest in bidirectional transformations (BXs) has led to the development of many BX frameworks, originating in diverse computer science disciplines. From a use…
Automatic Unbounded Verification of Alloy Specifications with Prover9
Nuno Macedo, Alcino Cunha
Alloy is an increasingly popular lightweight specification language based on relational logic. Alloy models can be automatically verified within a bounded scope using off-the-shelf…