Software Abstractions - Logic, Language, and Analysis

By Daniel Jackson. 2006

1,910 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Information Systems

View Paper: https://www.semanticscholar.org/paper/1a52ce430a6146194861979828cd1961a416f3a7

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

Citations in the corpus

Essence: A constraint language for specifying combinatorial problems (2008, background): “The Alloy language [20] avoids some of these shortcomings of Z by restricting itself to first-order logic.”
Building a push-button RESOLVE verifier: Progress and challenges (2011, neutral): “, that adding an element to a queue increases the length of the queue by one (without stipulating anything about, for example, the order of the actual queue elements) [40]; or (c) a complete behavioral specification of what the software is supposed to do and what it is not supposed to do [1][28][37]”
The Oracle Problem in Software Testing: A Survey (2015, background): “in the literature [101], [109], [182], [183].”
Self-Managed Systems: an Architectural Challenge (2007, methodology): “For example, in our system described in [23], we specified system structural constraints in Alloy [26] and developed tactics that could be shown using the Alloy model checker to move a system into a state that satisfied constraints.”
Research Directions in Requirements Engineering (2007, background): “Verification models, expressed in these notations, are simplifications and abstractions of a specification to be verified [22, 51, 89].”
UML2Alloy: a challenging model transformation (2007, methodology): “One solution, which has been proposed is to introduce the notion of a state at the model level [5,25].”
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (2010, methodology): “This flaw was already detected by Jackson using the Alloy Analyzer on his original specification and can be fixed by adding k′ ' curr s r to the conjunction in ENTRY.”
Verdi: a framework for implementing and formally verifying distributed systems (2015, methodology): “For example, Zave applied Alloy [15] to analyzing the protocol of the Chord distributed hash table [43].”
Software model checking (2009, positive): “Bounded model generation ideas have also been used to check consistency of abstract speciﬁcations, most notably in the Alloy analyzer [Jackson 2006].”