This experience report describes a style of applying symbolic model checking developed
over the course of four years at Amazon Web Services (AWS). Lessons learned are drawn …

Alloy is a declarative formal modeling language with syntax derived from notations common
to object-oriented design and first-order relational logic semantics. To better understand the …

Formal verification of software is a bit of a niche activity: it is only applied to the most safety-
critical or security-critical software and it is typically only performed by specialized …

This article describes a style of applying symbolic model checking developed over the
course of four years at Amazon Web Services (AWS). Lessons learned are drawn from …

This paper proposes the first mutation-based technique for the repair of Alloy 6 first-order
temporal logic specifications. This technique was developed with the educational context in …

Programming tools are increasingly integral to research and analysis in myriad domains,
including specialized areas with no formal relation to computer science. Embedded domain …

Formal verification has become increasingly crucial in ensuring the accurate and secure
functioning of modern software systems. Given a specification of the desired behaviour, ie a …

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive
system from its temporal logic specification. Despite its attractiveness and major research …

Background: Many programming environments include automated feedback in the form of
hints to help novices learn autonomously. Some experimental studies investigated the …

This contribution proposes to apply informal ideas for model development within a formal
tool. The basic idea is to relax the requirements expressed with particular modeling …