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

UML

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 - dl.acm.org
UML2Alloy: A tool for lightweight modelling of Discrete Event Systems	B Bordbar… - IADIS International Conference in …, 2005 - imamu.edu.sa<
A model driven approach for the automated analysis of UML class diagrams	K Anastasakis - 2009 - kyriakos.anastasakis.net
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 - jot.fm
Secrecy UML method for model transformations	W Hassan, N Slimani, K Adi… - 2nd International Conference …, 2010 - w3.uqo.ca
Business process modeling and formal verification	M Wu - Journal of Zhejiang University. Engineering Science, 2011 - csa.com
A UML class diagram analyzer	T Massoni, R Gheyi… - TUM, 2004 - sse-tubs.de
Transforming OntoUML into Alloy: towards conceptual model validation using a lightweight formal method	BFB Braga, JPA Almeida, G Guizzardi… - Innovations in Systems …, 2010 - Springer

i*

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 - books.google.com

KM3

Model search: Formalizing and automating constraint solving in mde platforms

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

CVL

Secrecy UML method for model transformations

W Hassan, N Slimani, K Adi… - 2nd International Conference …, 2010 - w3.uqo.ca

Formal Specification Languages

Event-B

PJ Matos… - Arxiv preprint arXiv:0805.3256, 2008 - arxiv.org

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

Z

Translating Z to Alloy

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

OCL

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 - sts.tu-harburg.de
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 - journal.ub.tu-berlin.de
A model-prover for constrained dynamic conversations	D Cacciagrano, F Corradini, R Culmone… - Proceedings of the 10th …, 2008 - dl.acm.org
Using Model Driven Engineering to Reliably Automate the Measurement of Object-Oriented Software	JA McQuillan - 2011 - eprints.nuim.ie

Theorem Proving Languages

KIV

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