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

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

[BOOK] 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

Model checking event-b by encoding into alloy

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

ACL2

Pythia: Automatic generation of counterexamples for ACL2 using Alloy

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

Isabelle

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

JC Blanchette - 2010 - in.tum.de

Architectural Languages

AADL

Verification of replication architectures in AADL

D de Niz... - Engineering of Complex Computer ..., 2009 - ieeexplore.ieee.org

Ontology Languages

OWL

Reasoning support for Semantic Web ontology family languages using Alloy

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

DAML+OIL

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