alloy as backend

Papers describing analysis of various languages by translation into Alloy, taken from first 400 results of query to Google scholar for papers that cite Alloy.

Modeling Languages


UML2Alloy: A challenging model transformation

K Anastasakis, B Bordbar, G Georg... - Model Driven Engineering ..., 2007 - Springer

From UML to Alloy and back again

S Shah, K Anastasakis... - Models in Software Engineering, 2010 - Springer

Verification of Aspect-UML models using Alloy

F Mostefaoui... - ... of the 10th international workshop on Aspect- ..., 2007 -

UML2Alloy: A tool for lightweight modelling of Discrete Event Systems

B Bordbar... - IADIS International Conference in ..., 2005 -

[BOOK] A model driven approach for the automated analysis of UML class diagrams

K Anastasakis - 2009 -

CD2Alloy: Class diagrams analysis using Alloy revisited

S Maoz, J Ringert... - Model Driven Engineering Languages and ..., 2011 - Springer

Understanding and improving UML package merge

J Dingel, Z Diskin... - Software and Systems Modeling, 2008 - Springer

Design-level Detection of Interactions in Aspect-UML models using Alloy

F Mostefaoui... - Journal of Object Technology, 2007 -

Secrecy UML method for model transformations

W Hassan, N Slimani, K Adi... - 2nd International Conference ..., 2010 -

Business process modeling and formal verification

M Wu - Journal of Zhejiang University. Engineering Science, 2011 -

A UML class diagram analyzer

T Massoni, R Gheyi... - TUM, 2004 -

Transforming OntoUML into Alloy: towards conceptual model validation using a lightweight formal method

BFB Braga, JPA Almeida, G Guizzardi... - Innovations in Systems ..., 2010 - Springer


Verification of i* Models Using Alloy

PO Ating'a... - Information Systems Development, 2011 - Springer

Using i* to Model Access Policies: Relating Actors to Their Organizational Context

R Crook, D Ince... - Social Modeling for ..., 2011 -


Model search: Formalizing and automating constraint solving in mde platforms

M Kleiner, M Del Fabro... - Modelling Foundations and ..., 2010 - Springer


Secrecy UML method for model transformations

W Hassan, N Slimani, K Adi... - 2nd International Conference ..., 2010 -

Formal Specification Languages


Model checking event-b by encoding into alloy

PJ Matos... - Arxiv preprint arXiv:0805.3256, 2008 -

Graph Transformation Languages

On the use of Alloy to analyze graph transformation systems

L Baresi... - Graph Transformations, 2006 - Springer

Tabular Specs

Describing and Analyzing Behaviours over Tabular Specifications Using (Dyn) Alloy

N Aguirre, M Frias, M Moscato, T Maibaum... - ... Approaches to Software ..., 2009 - Springer


Translating Z to Alloy

P Malik, L Groves... - Abstract State Machines, Alloy, B and Z, 2010 - Springer


An aspect-oriented methodology for designing secure applications

G Georg, I Ray, K Anastasakis, B Bordbar... - Information and software ..., 2009 - Elsevier

Formalization of QVT-Relations: OCL-based static semantics and Alloy-based validation

M Garcia - Proceedings of the Second Workshop on MDSD ..., 2008 -

Extensive validation of OCL models by integrating SAT solving into USE

M Kuhlmann, L Hamann... - Objects, Models, Components, ..., 2011 - Springer

Executing Underspecified OCL Operation Contracts with a SAT Solver

MP Krieger... - Electronic Communications of the ..., 2008 -

A model-prover for constrained dynamic conversations

D Cacciagrano, F Corradini, R Culmone... - Proceedings of the 10th ..., 2008 -

Using Model Driven Engineering to Reliably Automate the Measurement of Object-Oriented Software

JA McQuillan - 2011 -

Theorem Proving Languages


Automating algebraic specifications of non-freely generated data types

A Dunets, G Schellhorn... - Automated Technology for Verification ..., 2008 - Springer

Automated Flaw Detection in Algebraic Specifications

A Dunets, G Schellhorn... - Journal of Automated Reasoning, 2010 - Springer


Pythia: Automatic generation of counterexamples for ACL2 using Alloy

A Spiridinov... - ... of the 7th International Workshop on the ..., 2007 -


Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod (System Description)

JC Blanchette - 2010 -

Architectural Languages


Verification of replication architectures in AADL

D de Niz... - Engineering of Complex Computer ..., 2009 -

Ontology Languages


Reasoning support for Semantic Web ontology family languages using Alloy

HH Wang, JS Dong, J Sun... - Multiagent and Grid Systems, 2006 - IOS Press


Non-standard Reasoning Services for the Verification of DAML+OIL Ontologies

Y Song, R Chen - IFIP Advances in Information and Communication Technology, 2010

Description Logics

Model Generation in Description Logics: What Can We Learn From Software Engineering

M Garcia, A Kaplunova, R Moller - 2007