3 papers
cs.SE2026
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…
cs.SE2026
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…
cs.SE2025
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…