Selected papers that describe applications of Alloy:

Papers on Teaching with Alloy

Teach foundational language principles Communications of the ACM Thomas Ball & Benjamin Zorn - 2015
Using Alloy in Introductory Courses of Formal Methods Structured Object-Oriented Formal Language and Method Shin Nakajima - 2014 - Springer
Introducing Alloy in a Software Modelling Course Formal Methods in Computer Science J Noble, DJ Pearce…, 2008.
Chief Chefs of Z to Alloy: Using a Kitchen Example to Teach Alloy with Z Teaching Formal Methods S Tarkan… - 2009
Workshop-modeling software the alloy way Frontiers in Education Conference (FIE) MJ Lutz…, 2013
Experiences of Teaching a Lightweight Formal Method Electronic Notes in Theoretical Computer Science RC Boyatt…, 2008
A Guide To Alloy   EYS Wong, M Herrmann…
Experiences with Alloy in undergraduate formal methods   M Lutz - 2006

Enterprise Modeling

A model-driven environment for service design, simulation and prototyping. Exploring Services Science Biljana Bajić-Bizumić & Claude Petitpierre & Hieu Chi Huynh et al. - 2013 - Springer
Simulation-Driven Approach for Business Rules Discovery. Advanced Information Systems Engineering Workshops Biljana Bajić-Bizumić & Irina Rychkova & Alain Wegmann - 2013
Support for Domain Constraints in the Validation of Ontologically Well-Founded Conceptual Models. Enterprise, Business-Process and Information Systems Modeling John Guerson & João Paulo A Almeida & Giancarlo Guizzardi - 2014
Alloy4SPV: A Formal Framework for Software Process Verification. Modelling Foundations and Applications Yoann Laurent & Reda Bendraou & Souheib Baarir et al. - 2014 - Springer
Debugging designs. 14th International Workshop on High Performance Transaction Systems, Monterey Chris Newcombe - 2011
Exploring the Alloy operational semantics for case management process modeling. Research Challenges in Information Science (RCIS), 2013 IEEE Seventh International Conference Irina Rychkova - 2013
An Example of a Hierarchical System Model Using SEAM and its Formalization in Alloy EDOC Workshop A Wegmann, LS Le, I Rychkova…, 2007


An Alloy Verification Model for Consensus-Based Auction Protocols. arXiv preprint arXiv:1407.5074 Saber Mirzaei & Flavio Esposito - 2014
Verifying dominant strategy equilibria in auctions Multi-Agent Systems and Applications V, 2007 E Tadjouddine…

Electronic Commerce

Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method Formal Aspects of Computing, 2008 - Springer T Ramananandro
An aspect oriented model of efficient and secure card-based payment system Proceedings of the 2011 International Conference DP Nigam…


Towards a formal foundation of web security. 23rd IEEE Computer Security Foundations Symposium Devdatta Akhawe & Adam Barth & Peifung E. Lam et al. - 2010
The Same-Origin Policy. 500 Lines or Less Eunsuk Kang & Santiago Perez De Rosso & Daniel Jackson - 2016
Enforcing spatio-temporal access control in mobile applications. Computing Ramadan Abdunabi & Wuliang Sun & Indrakshi Ray - 2014 - Springer
Toward a lightweight model of BGP safety. Proc. of WRiPE Matvey Arye & Rob Harrison & Richard Wang et al. - 2011
Automated dynamic enforcement of synthesized security policies in android   Hamid Bagheri & Alireza Sadeghi & Reyhaneh Jabbarvand et al. - 2015
Network and Web Security Modeling and Analysis   Jason Bau - 2014
A Viewpoint-Based Approach for Formal Safety & Security Assessment of System Architectures. 11th Workshop on Model-Driven Engineering, Verification and Validation Julien Brunel & David Chemouil & Laurent Rioux et al. - 2014
Formal safety and security assessment of an avionic architecture with Alloy arXiv preprint arXiv:1405.1113 Julien Brunel & Laurent Rioux & Stéphane Paul et al. - 2014
Modeling and Verification of Redundancy Policies. ACESMB@ MoDELS Hamza Chouh & Charlotte Callon & Ghita Jalal et al. - 2013
Formal model-based validation for tally systems. E-Voting and Identify Dermot Cochran & Joseph R Kiniry - 2013 - Springer
Formalizing Security Aspects of the Web Platform in Alloy   Daniel Fett & Ralf Küsters - 2011
Model-driven approaches to analysing time-and location-dependent access control specifications   Emsaieb Mosbah Geepalla - 2013
Using model driven security approaches in web application development. Information and Communication Technology Christoph Hochreiner & Zhendong Ma & Peter Kieseberg et al. - 2014 - Springer
Modeling Multiple Modes of Operation with Alloy. Computer Applications for Security, Control and System Engineering Christos Kalyvas & Elisavet Konstantinou & Georgios Kambourakis - 2012 - Springer
A Lightweight Formal Approach for Analyzing Security of Web Protocols. Research in Attacks, Intrusions and Defenses Apurva Kumar - 2014 - Springer
Managing trust and secrecy in identity management clouds. Proceedings of the 2012 ACM Workshop on Cloud computing security workshop Apurva Kumar - 2012
Using automated model analysis for reasoning about security of web protocols. Proceedings of the 28th Annual Computer Security Applications Conference Apurva Kumar - 2012
Security analysis of bytecode interpreters using alloy   Mark Clifford Reynolds & Assaf J Adviser-Kfoury - 2012 - Boston University
CORP: A Browser Policy to Mitigate Web Infiltration Attacks. Information Systems Security Krishna Chaitanya Telikicherla & Venkatesh Choppella & Bruhadeshwar Bezawada - 2014 - Springer
Validation of a Security Model with the Alloy Analyzer   PS Grisham, CL Chen, S Khurshid… - 2008 -
Modeling partial attacks with Alloy Security Protocols, 2010 - Springer A Lin, M Bond…
Lightweight Modeling of Java Virtual Machine Security Constraints Abstract State Machines, Alloy, B and Z, 2010 - Springer M Reynolds
Using Lightweight Formal Methods for JavaScript Security   M Reynolds - 2010 -
A Lightweight Formal Analysis of a Multicast Key Management Scheme IFIP Lecture Notes in Computer Science (LNCS), 2011 - D Jackson…
A security domain model for implementing Trusted Subject Behaviors   M Auguston, A Shaffer - 2008
Formal Models of a Least Privilege Separation Kernel in Alloy   M Auguston, TE Levin… - 2008
A security domain model for static analysis and verification of software programs 2007 - DTIC Document A Shaffer

Access Control and Security Policies

Using i* to Model Access Policies: Relating Actors to Their Organizational Context. Social Modeling for Requirements Engineering Robert Crook & Darrel Ince & Bashar Nuseibeh - 2011 - MIT Press
Early security patterns: A collection of constraints to describe regulatory security requirements Requirements Patterns (RePa), 2012 IEEE Second International Workshop on Robin A Gandhi & Mariam Rahmani - 2012
An Automated Approach to Detect Inconsistency and Semi-consistency Spatio-Temporal Role Based Access Control Specification. Journal of Data Processing Emsaieb Geepalla & Behzad Bordbar - 2012
On formalizing of inconsistency and semi-consistency in spatio-temporal access control. Digital Information Management (ICDIM), 2012 Seventh International Conference on Emsaieb Geepalla & Behzad Bordbar - 2012
Spatio-Temporal Role Based Access Control for Physical Access Control Systems. Emerging Security Technologies (EST), 2013 Fourth International Conference on Emsaieb Geepalla & Behzad Bordbar & Xiaofeng Du - 2013
Transformation of spatio-temporal role based access control specification to alloy. Model and Data Engineering Emsaieb Geepalla & Behzad Bordbar & Joel Last - 2012 - Springer
Role-Based Access Control modeling and validation. ISCC Ramzi A Haraty & Mirna Naous - 2013
Assuring consistency in mixed models. Journal of Computational Science Ramzi A Haraty & Mirna F Naous & Azzam Mourad - 2014 - Elsevier
Security analysis of temporal RBAC under an administrative model. Computers & Security Sadhana Jha & Shamik Sural & Jaideep Vaidya et al. - 2014 - Elsevier
A Novel Trusted Hierarchy Construction for RFID-Sensor Based MANETs Using ECC. Electronics and Telecommunications Research Institute Journal Adarsh Kumar & Krishna Gopal & Alok Aggarwal - 2014
Automatic conformance checking of role-based access control policies via alloy Engineering Secure Software and Systems David Power & Mark Slaymaker & Andrew Simpson - 2011 - Springer
Conformance checking of dynamic access control policies Formal Methods and Software Engineering David Power & Mark Slaymaker & Andrew Simpson - 2011 - Springer
Specification and Verification Using Alloy of Optimistic Access Control for Distributed Collaborative Editors Formal Methods for Industrial Critical Systems Aurel Randolph & Abdessamad Imine & Hanifa Boucheneb et al. - 2013 - Springer
Formal Verification of Cross-Domain Access Control Policies Using Model Checking   Mark C Reynolds & Azer Bestavros - 2011 - Citeseer
PCIEF: a policy conflict identification and evaluation framework International Journal of Information and Computer Security Vimalathithan Subramanian & Remzi Seker & Srini Ramaswamy et al. - 2012 - Inderscience
Rigorous analysis of uml access control policy models Policies for Distributed Systems and Networks (POLICY),2011 IEEE International Symposium on Wuliang Sun & Robert France & Indrakshi Ray - 2011
Alloy model for Cross Origin Request Policy (CORP)   Krishna Chaitanya Telikicherla & Venkatesh Choppella - 2013
Using Automated Model Analysis for Reasoning about Security of web protocols   Apurva Kumar - 2012 - IBM Research India
Rigorous Analysis of UML Access Control Policy Models   W Sun, R France… - Policies for Distributed Systems and …, 2011 -
Automatic conformance checking of role-based access control policies via alloy   D Power, M Slaymaker… - Engineering Secure Software and …, 2011 - Springer
Conformance checking of dynamic access control policies Formal Methods and Software …, 2011 - Springer D Power, M Slaymaker…
Enabling verification and conformance testing for access control model Proceedings of the 13th ACM Symposium on Access …, 2008 - H Hu…
Verification of policy-based self-managed cell interactions using alloy Filho, E Lupu, M Sloman… - … and Networks, 2009. …, 2009 - A Schaeffe
Ensuring spatio-temporal access control for real-world applications Proceedings of the 14th …, 2009 - M Toahchoodee, I Ray, K Anastasakis…
Formal verification of OAuth 2.0 using Alloy framework … Systems and Network …, 2011 - S Pai, Y Sharma, S Kumar…
Conformance verification of privacy policies Web Services and Formal Methods, 2011 - Springer X Fu
Formalising and validating RBAC-to-XACML translation using lightweight formal methods Abstract State Machines, Alloy, B …, 2010 - Springer M Slaymaker, D Power…
A Formal Method Based Case Study for Access Control Computational Intelligence and …, 2009 G Li, Y Xiao, M Lu… -
On the modelling and analysis of Amazon Web Services access policies A Proof based approach …, 2009 D Power, A Simpson…
New Approach for Testing the Correctness of Access Control Policies 2009 - S Sharma…
An Application of Alloy to Static Analysis for Secure Information Flow and Verification of Software Systems 2008 - DTIC Document AB Shaffer

Feature Modeling and Analysis

Feature and meta-models in Clafer: mixed, specialized, and coupled Software Language Engineering Kacper Bąk & Krzysztof Czarnecki & Andrzej Wąsowski - 2011 - Springer
Supporting Multi-Level Configuration with Feature-Solution Graphs: Formal Semantics and Alloy implementation   Jaime Chavarriaga & Carlos Noguera & Rubby Casallas et al. - 2013
Translating the Feature-Oriented Requirements Modelling Language to Alloy   David Dietrich & Pourya Shaker & Jan Gorzny et al. - 2012
Pairwise testing for software product lines: comparison of two approaches Software Quality Journal Gilles Perrouin & Sebastian Oster & Sagar Sen et al. - 2012 - Springer
Feature and class models in Clafer: Mixed, specialized, and coupled … on Software Language …, 2010 - K Bak, K Czarnecki…
Detecting dependences and interactions in feature-oriented design … (ISSRE), 2010 IEEE …, 2010 - S Apel, W Scholz, C Lengauer…
Variability modeling and qos analysis of web services orchestrations Web Services (ICWS), …, 2010 - A Kattepur, S Sen, B Baudry…

Domain Specific Languages and Modeling

Supervisory control theory with Alloy Science of Computer Programming Benoit Fraikin & Marc Frappier & Richard St-Denis - 2014 - Elsevier
Modeling the supervisory control theory with Alloy Abstract State Machines, Alloy, B, VDM, and Z Benoit Fraikin & Marc Frappier & Richard St-Denis - 2012 - Springer
Using alloy to support feature-based DSL construction for mining software repositories Proceedings of the 17th International Software Product Line Conference co-located workshops Changyun Huang & Yasutaka Kamei & Kazuhiro Yamashita et al. - 2013
aRby: An Embedding of Alloy in Ruby Abstract State Machines, Alloy, B, TLA, VDM, and Z  
Aleksandar Milicevic & Ido Efrati & Daniel Jackson - 2014 - Springer    
Verification of DSMLs using graph transformation: a case study with Alloy … Workshop on Model-Driven …, 2009 - Z Demirezen, M Mernik, J Gray…

Train Control

Specifying a Testing Oracle for Train Stations–Going beyond with Product Line Technology Models in Software Engineering Andreas Svendsen & Øystein Haugen & Birger Møller-Pedersen - 2012 - Springer
Specifying a testing oracle for train stations Proceedings of the 8th International Workshop on Model-Driven Engineering, Verification and Validation Andreas Svendsen & Øystein Haugen & Birger Møller-Pedersen - 2011
Model based specification validation for automatic train protection and block system Computing and Convergence Technology (ICCCT), 2012 7th International Conference on Guo Xie & Xinhong Hei & Hiroshi Mochizuki et al. - 2012
Formalizing train control language: automating analysis of train stations in Railways XII: …, 2010 A Svendsen, B Møller-Pedersen…

File Systems

Formal modeling and analysis of a flash filesystem in Alloy Abstract state machines, B and Z, 2008 - Springer E Kang…
Variations on an Alloy-centric tool-chain in verifying a journaled file system model 2010 - MA Ferreira…
Verifying Intel flash file system core specification … in VDM: Proceedings of the Fourth …, 2008 - MA Ferreira, SS Silva…

Software Architecture

A Formal Approach for Incorporating Architectural Tactics into the Software Architecture. SEKE Hamid Bagheri & Kevin J Sullivan - 2011
Efficient re-resolution of SMT specifications for evolving software architectures Proceedings of the 10th international ACM Sigsoft conference on Quality of software architectures Kenneth Johnson & Radu Calinescu - 2014
CD2Alloy: Class diagrams analysis using Alloy revisited Model Driven Engineering Languages and Systems Shahar Maoz & Jan Oliver Ringert & Bernhard Rumpe - 2011 - Springer
Analyzing variability: capturing semantic Ripple effects Modelling Foundations and Applications Andreas Svendsen & Øystein Haugen & Birger Møller-Pedersen - 2011 - Springer
A Lightweight Modeling and Verifying Method for Dynamic Evolution of Software Architectures Using Alloy. Journal of Convergence Information Technology Hongzhen Xu & Guosun Zeng - 2013
Model checking software architecture design High-Assurance Systems Engineering (HASE), 2012 IEEE 14th International Symposium on Jiexin Zhang & Yang Liu & Jing Sun et al. - 2012
Monarch: Model-based development of software architectures Model Driven Engineering Languages and …, 2010 - Springer H Bagheri, K Sullivan
Dynamic software architectures verification using DynAlloy Electronic Communications of …, 2008 - A Bucchiarone…
A formal specification of the Fractal component model in Alloy 2008 - P Merle, JB Stefani
Assessing Component’s Behavioral Interoperability Concerning Goals On the Move to Meaningful Internet Systems: …, 2008 - Springer W Ma, L Chung… -
A middleware model in alloy for supply chain-wide agent interactions Agent-Oriented …, 2011 - Springer R Haesevoets, D Weyns, M Cruz Torres…
Modeling and analyzing architectural change with alloy Proceedings of the 2010 ACM Symposium on …, 2010 - dl.acm.or KM Hansen… g
Modeling and analysis of Reo connectors using Alloy … Models and Languages, 2008 - Springer R Khosravi, M Sirjani, N Asoudeh, S Sahebi…
Graph-based design and analysis of dynamic software architectures … , Graphs and Models, 2008 - Springer R Bruni, A Bucchiarone, S Gnesi, D Hirsch…
Towards self-management in service-oriented computing with modes Service-Oriented Computing- …, 2009 - Springer H Foster, S Uchitel, J Kramer…
Dynamic software architectures for global computing systems 2008 - A Bucchiarone
A model transformation approach to derive architectural models from goal-oriented requirements models On the Move to …, 2009 - Springer M Lucena, J Castro, C Silva, F Alencar…
Specifying Self-configurable Component-Based Systems with FracToy Abstract State Machines, Alloy, B …, 2010 - Springer A Tiberghien, P Merle…
Analyzing architectural styles Journal of Systems and Software, 2010 - Elsevier JS Kim…
Verification of replication architectures in AADL Engineering of Complex Computer …, 2009 D de Niz… g
Architectural style as an independent variable Proceedings of the IEEE/ACM …, 2010 H Bagheri, Y Song…


Synchronizing model and program refactoring Formal methods: foundations and applications Tiago Massoni & Rohit Gheyi & Paulo Borba - 2011 - Springer
UML model refactoring: a systematic literature review Empirical Software Engineering Mohammed Misbhauddin & Mohammad Alshayeb - 2013 - Springer
Automated behavioral testing of refactoring engines Software Engineering, IEEE Transactions on Gustavo Soares & Rohit Gheyi & Tiago Massoni - 2013 - IEEE
Identifying overly strong conditions in refactoring implementations Software Maintenance (ICSM), 2011 27th IEEE International Conference on Gustavo Soares & Melina Mongiovi & Rohit Gheyi - 2011
Analyzing Behavioral Refactoring of Class Models. ME@ MoDELS Wuliang Sun & Robert B France & Indrakshi Ray - 2013
Alloy as a Refactoring Checker? Electronic Notes in Theoretical Computer …, 2008 - Elsevier H Estler, H Wehrheim
Sound Object Model Refactorings 2010 - R Gheyi…
Toward a Formal Evaluation of Refactorings Formal Methods …, 2008 - J Paul, N Kuzmina, R Gamboa…
Formal model-driven program refactoring Proceedings of the Theory and practice …, 2008 - T Massoni, R Gheyi…
Synchronizing model and program refactoring Formal Methods: Foundations and …, 2011 - Springer T Massoni, R Gheyi…

Program verification

Verification of i* models using alloy Information Systems Development Peter Oluoch Ating’a & Aneesh Krishna - 2011 - Springer
Verification of ATL transformations using transformation models and model finders Formal Methods and Software Engineering Fabian Büttner & Marina Egea & Jordi Cabot et al. - 2012 - Springer
Optimized translation of clafer models to alloy   Kacper Bak - 2011
SEFM: software engineering and formal methods Software & Systems Modeling Gilles Barthe & Alberto Pardo & Gerardo Schneider - 2014 - Springer
Data Model Bugs NASA Formal Methods Ivan Bocić & Tevfik Bultan - 2015 - Springer
Automated specification analysis using an interactive theorem prover Formal Methods in Computer-Aided Design (FMCAD), 2011 Harsh Raju Chamarthi & Panagiotis Manolios - 2011
Practical JFSL verification using TACO Software: Practice and Experience M Chicote & Daniel Ciolek & Juan Pablo Galeotti - 2014 - Wiley Online Library
Model checking support for conflict resolution in multiple non-functional concern management Euro-Par 2011: Parallel Processing Workshops Marco Danelutto & Peter Kilpatrick & Carlo Montangero et al. - 2012
Empirical comparison and performance evaluation of adequacy criteria for testing database application   Jitendra D Deshmukh - 2012 - Jhunjhunu
Relational reasoning via SMT solving FM 2011: Formal Methods Aboubakr Achraf El Ghazi & Mana Taghdiri - 2011 - Springer
Specifying UML protocol state machines in Alloy Integrated Formal Methods Ana Garis & Ana CR Paiva & Alcino Cunha et al. - 2012
A dual-engine for early analysis of critical systems arXiv preprint arXiv:1408.0707 Aboubakr Achraf El Ghazi & Ulrich Geilmann & Mattias Ulbrich et al. - 2014
Behavioral validation of JFSL specifications through model synthesis Proceedings of the 34th International Conference on Software Engineering Carlo Ghezzi & Andrea Mocci - 2012
Checking Transformation Model Properties with a UML and OCL Model Validator Proc. 3rd Int. STAF’2014 Workshop Verification of Model Transformations (VOLT’2014) Martin Gogolla & Lars Hamann & Frank Hilken - 2014
Generating JML Specifications from Alloy Expressions Hardware and Software: Verification and Testing Daniel Grunwald & Christoph Gladisch & Tianhai Liu et al. - 2014 - Springer
Formalization of fUML: An Application to Process Verification Advanced Information Systems Engineering Yoann Laurent & Reda Bendraou & Souheib Baarir et al. - 2014
Formal verification of Pastry using TLA+ International Workshop on the TLA+ Method and Tools Tianxiang Lu & Stephan Merz & Christoph Weidenbach - 2012
Symbolic execution for (almost) free: Hijacking an existing implementation to perform symbolic execution   Joseph P Near & Daniel Jackson - 2014
Rubicon: bounded verification of web applications Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering Joseph P Near & Daniel Jackson - 2012
How Amazon web services uses formal methods Communications of the ACM Chris Newcombe & Tim Rath & Fan Zhang et al. - 2015 - ACM
An integrated data model verifier with property templates Formal Methods in Software Engineering (FormaliSE), 2013 1st FME Workshop on Jaideep Nijjar & Ivan Bocic & Tevfik Bultan - 2013
Unbounded data model verification using SMT solvers Automated Software Engineering (ASE), 2012 Proceedings of the 27th IEEE/ACM International Conference on Jaideep Nijjar & Tevfik Bultan - 2012
Alloy meets the algebra of programming: A case study Software Engineering, IEEE Transactions on Jose N Oliveira & Miguel A Ferreira - 2013 - IEEE
A dataflow analysis to improve sat-based bounded program verification Software Engineering and Formal Methods Bruno Cuervo Parrino & Juan Pablo Galeotti & Diego Garbervetsky et al. - 2011 - Springer
OCL-Lite: Finite reasoning on UML/OCL conceptual schemas Data & Knowledge Engineering Anna Queralt & Alessandro Artale & Diego Calvanese et al. - 2012 - Elsevier
Modeling the Java Bytecode Verifier Science of Computer Programming Mark C Reynolds - 2013 - Elsevier
Parallel bounded analysis in code with rich invariants by refinement of field bounds Proceedings of the 2013 International Symposium on Software Testing and Analysis Nicolás Rosner & Juan Galeotti & Santiago Bermúdez et al. - 2013
Finding errors from reverse-engineered equality models using a constraint solver Software Maintenance (ICSM), 2012 28th IEEE International Conference on Chandan Raj Rupakheti & Daqing Hou - 2012
Towards a methodology for verifying partial model refinements Software Testing, Verification and Validation (ICST), 2012 IEEE Fifth International Conference on Rick Salay & Marsha Chechik & Jan Gorzny - 2012
Model transformation specification for automated formal verification Software Engineering (MySEC), 2011 5th Malaysian Conference in Asmiza Abdul Sani & Fiona AC Polack & Richard F Paige - 2011
Trans-DV: A Framework for Developing and Formally Verifying Model Transformation Specifications Sponsoring Institutions Asmiza A Sani & Fiona AC Polack & Richard F Paige - 2011
Specification and Verification of Graph-Based Model Transformation Properties Graph Transformation Gehan MK Selim & Levi Lúcio & James R Cordy et al. - 2014 - Springer
A feedback technique for unsatisfiable UML/OCL class diagrams Software: Practice and Experience Asadullah Shaikh & Uffe Kock Wiil - 2014 - Wiley Online Library
Analyzing temporal properties of abstract models Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering Amirhossein Vakili - 2011
Reducing CTL-live Model Checking to First-Order Logic Validity Checking Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design Amirhossein Vakili & Nancy A Day - 2014
Verification of model transformations using Alloy PAMT 2014 Xiaoliang Wang - 2014
Scalable Verification of Model Transformations 11th Workshop on Model Driven Engineering, Verification and Validation MoDeVVa 2014 Xiaoliang Wang & Adrian Rutle & Yngve Lamo - 2014
How To Make Chord Correct   Pamela Zave - 2014
Verifying specifications with associated attributes in graph transformation systems Frontiers of Computer Science Yu Zhou & Yankai Huang & Ou Wei et al. - 2015 - Springer
Equals Checker 2011 - CR Rupakheti…
A Security Domain Model for Static Analysis and Verification of Software Programs Proceedings of the 20th …, 2008 AB Shaffer, M Auguston, C Irvine…
Analyzing Ruby on Rails Data Models using Alloy GSWC 2010, 2010 - J Nijjar…
Analysis of invariants for efficient bounded verification Proceedings of the 19th …, 2010 - JP Galeotti, N Rosner, CG Lopez Pombo…
Automatic code generation and solution estimate for object-oriented embedded software Companion to the 23rd ACM SIGPLAN conference on …, 2008 RR Ferreira
Formal Logic Based Configuration Modeling and Verification for Dynamic Component Systems MOPAS 2011, The Second …, 2011 - Z Theisz, G Batori…
An Abstraction-Oriented, Path-Based Approach for Analyzing Object Equality in Java Reverse Engineering (WCRE), 2010 …, 2010 - CR Rupakheti…


Systematic testing of database engines using a relational constraint solver Software Testing, Verification and Validation (ICST), 2011 IEEE Fourth International Conference on Shadi Abdul Khalek & Sarfraz Khurshid - 2011
Bounded verification of Ruby on Rails data models Proceedings of the 2011 International Symposium on Software Testing and Analysis Jaideep Nijjar & Tevfik Bultan - 2011
A Framework for Verifying Consistency of SQL-DB Ontology using Alloy Conference: 16th Korea Computer Congress Isma Farah Siddiqui & Scott Uk-Jin Lee - 2014
Mapping between Alloy specifications and database implementations Software Engineering and Formal …, 2009 - A Cunha…
Towards an Alloy Formal Model for Flexible Advanced Transactional Model Development 2009 B Gallina…

Model-Driven Development

Automated Composition of Sequence Diagrams via Alloy. MODELSWARD Mohammed Alwanain & Behzad Bordbar & Juliana Küster Filipe Bowles - 2014
A model driven approach to analysis and synthesis of sequence diagrams   Mohamed Ariff Ameedeen - 2012
Bottom-up model-driven development Software Engineering (ICSE), 2013 35th International Conference on Hamid Bagheri & Kevin Sullivan - 2013
Metamodel based methodology for dynamic component systems Modelling Foundations and Applications Gabor Batori & Zoltan Theisz & Domonkos Asztalos - 2012 - Springer
Translating between Alloy specifications and UML class diagrams annotated with OCL Software & Systems Modeling Alcino Cunha & Ana Garis & Daniel Riesco - 2013 - Springer
Automatic Unbounded Verification of Alloy Specifications with Prover9   Alcino Cunha & Nuno Macedo - 2011
Supporting model based design Model and Data Engineering Rémi Delmas & David Doose & Anthony Fernandes Pires et al. - 2011 - Springer
A verification and validation process for model-driven engineering Progress in Flight dynamics, guidance, navigation, control, fault detection, and avionics Rémi Delmas & A Fernandes Pires & Thomas Polacsek - 2013
Combining formal verification environments and model-driven engineering   Selma Djeddai - 2013
Chaining model transformations Proceedings of the First Workshop on the Analysis of Model Transformations Anne Etien & Vincent Aranega & Xavier Blanc et al. - 2012
ConceVE: Conceptual modeling and formal validation for everyone ACM Transactions on Modeling and Computer Simulation (TOMACS) Ross Gore & Saikou Diallo & Jose Padilla - 2014 - ACM
Lightweight formalization and validation of ORM models Journal of Logical and Algebraic Methods in Programming Amir Jahangard-Rafsanjani & Seyed-Hassan Mirian-Hosseinabadi - 2015 - Elsevier
Model-driven development meets security: An evaluation of current approaches System Sciences (HICSS), 2011 44th Hawaii International Conference on Kresimir Kasal & Johannes Heurix & Thomas Neubauer - 2011
Translating vdm to alloy Integrated Formal Methods Kenneth Lausdahl - 2013
Solving Clafer Models with Choco   Jimmy Liang - 2012 - GSDLab-TR
Implementing QVT-R bidirectional model transformations using Alloy Fundamental Approaches to Software Engineering Nuno Macedo & Alcino Cunha - 2013 - Springer
A manifesto for semantic model differencing Models in Software Engineering Shahar Maoz & Jan Oliver Ringert & Bernhard Rumpe - 2011 - Springer
Solving Design Tasks in Engineering Using Object-Oriented Graph-Based Representations and Boolean Satisfiability ASME 2013 International Design Engineering Technical Conferences and Computers and Information in Engineering Conference Clemens Munzer & Kristina Shea & Bergen Helms - 2013
Challenges in Integrating the Analysis of Multiple Non-Functional Properties in Model-Driven Software Engineering Proceedings of the 2015 Workshop on Challenges in Performance Methods for Software Development Dorina C Petriu - 2015
Transform both sides model: A parametric approach Computational Statistics & Data Analysis A Polpo & CP De Campos & D Sinha et al. - 2014 - Elsevier
Towards Testing Model Transformation Chains Using Precondition Construction in Algebraic Graph Transformation AMT 2014–Analysis of Model Transformations Workshop Proceedings Elie Richa & Etienne Borde & Laurent Pautet et al. - 2014
Supporting Iterative Development of Robust Operation Contracts in UML Requirements Models High-Assurance Systems Engineering (HASE), 2011 IEEE 13th International Symposium on Wuliang Sun & Robert B France & Indrakshi Ray - 2011
Systematic diagram refinement for code generation in SEAM Knowledge and Systems Engineering (KSE), 2012 Fourth International Conference on Quan Thanh Tho & others - 2012
Model transformation analysis: Staying ahead of the maintenance nightmare Theory and Practice of Model Transformations Marcel F Van Amstel & Mark GJ Van Den Brand - 2011 - Springer
Assessing the Kodkod model finder for resolving model inconsistencies Modelling Foundations and Applications Ragnhild Van Der Straeten & Jorge Pinna Puissant & Tom Mens - 2011 - Springer
Systematic scenario-based analysis of UML design class models Engineering of Complex Computer Systems (ICECCS), 2012 17th International Conference on Lijun Yu & Robert B France & Indrakshi Ray et al. - 2012
Developing Model-Driven Software Product Lines   Xiaorui Zhang - 2014
A manifesto for semantic model differencing Models in Software Engineering, 2011 - Springer S Maoz, J Ringert…
A lightweight approach for defining the formal semantics of a modeling language Model Driven Engineering Languages and Systems, 2008 - Springer P Kelsen…
Assessing the Kodkod model finder for resolving model inconsistencies Modelling Foundations and …, 2011 - Springer R Van Der Straeten, J Pinna Puissant…

Network Protocols

Modeling and analysis of RFID authentication protocols for supply chain management Parallel, Distributed and Grid Computing (PDGC), 2014 International Conference on Adarsh Kumar & Krishna Gopal & Alok Aggarwal - 2014
Simulation and analysis of authentication protocols for mobile Internet of Things (MIoT) Parallel, Distributed and Grid Computing (PDGC), 2014 International Conference on Adarsh Kumar & Krishna Gopal & Alok Aggarwal - 2014
Detecting Network Policy Conflicts Using Alloy Abstract State Machines, Alloy, B, TLA, VDM, and Z Ferney A Maldonado-Lopez & Jaime Chavarriaga & Yezid Donoso - 2014 - Springer
Using Alloy to Formally Model and Reason About an OpenFlow Network Switch Computer Science Department, Boston University, Tech. Rep Saber Mirzaei & Sanaz Bahargam & Richard Skowyra et al. - 2013
Formal verification of oauth 2.0 using alloy framework Communication Systems and Network Technologies (CSNT), 2011 Suhas Pai & Yash Sharma & Sunil Kumar et al. - 2011
A (not) nice way to verify the OpenFlow switch specification: formal modelling of the OpenFlow switch using alloy ACM SIGCOMM Computer Communication Review Natali Ruchansky & Davide Proserpio - 2013
Formal analysis of pure-join model of chord using alloy Software Engineering and Service Science (ICSESS), 2013 4th IEEE International Conference on Hooman Sadeghian & Alborz Samadi & Hassan Haghighi - 2013
A formal approach to the design and implementation of configuration strategy automation for switch network Journal of Tsinghua University Science and Technology Jiahai Yang & Ning Jiang & Changqing An et al. - 2012 - Tsinghua University Press, Tsinghua University Beijing 100084 China
How to Make Chord Correct (Using a Stable Base) arXiv preprint arXiv:1502.06461 Pamela Zave - 2015
Compositional Models of Network Architecture   Pamela Zave - 2014
Using lightweight modeling to understand chord ACM SIGCOMM Computer Communication Review Pamela Zave - 2012 - ACM
Compositional network mobility Verified Software: Theories, Tools, Experiments Pamela Zave & Jennifer Rexford - 2014 - Springer
Toward a lightweight model of BGP safety Int Workshop on Rigorous Protocol Engineering 2011 M Arye, R Harrison, R Wang, P Zave, J Rexford
Using Lightweight Modeling To Understand Chord 2009 - P Zave
Analyzing the Fundamental Liveness Property of the Chord Protocol 2018 - HAL open science J Brunel, D Chemouil, J Tawa
Reasoning about Identifier Spaces: How to make Chord Correct 2011 - P Zave
Compositional binding in network domains International Symposium on Formal Methods, 2006 - P Zave
A formal model of addressing for interoperating networks International Symposium of Formal Methods Europe, 2005 P Zave

Testing and Automated Test Case Generation

Improving test generation under rich contracts by tight bounds and incremental SAT solving Software Testing, Verification and Validation (ICST), 2013 IEEE Sixth International Conference on Pablo Abad & Nazareno Aguirre & Valeria Bengolea et al. - 2013
BloomUnit: Declarative testing for distributed programs Proceedings of the Fifth International Workshop on Testing Database Systems Peter Alvaro & Andrew Hutchinson & Neil Conway et al. - 2012
Specification-driven unit test generation for java generic classes Integrated Formal Methods Francisco Rebello de Andrade & Joao P Faria & Antónia Lopes et al. - 2012
Test Generation from Bounded Algebraic Specifications using Alloy. ICSOFT (2) Francisco Rebello de Andrade & João Pascoal Faria & Ana CR Paiva - 2011
ACM SIGSOFT Impact Paper Award 2012: Systematic Software Testing: The Korat Approach Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering Chandrasekhar Boyapati & Sarfraz Khurshid & Darko Marinov - 2012
CEGPairGen: An Automated Tool for Generating Pairwise Tests from Cause-Effect Graphs International Journal of Software Engineering and Its Applications Insang Chung - 2015
Model-based conformance testing for android Advances in Information and Computer Security Yiming Jing & Gail-Joon Ahn & Hongxin Hu - 2012 - Springer
JTACO: Test Execution for Faster Bounded Verification Tests and Proofs Alexander Kampmann & Juan Pablo Galeotti & Andreas Zeller - 2014 - Springer
Generating semantically valid test inputs using constrained input grammars Information and Software Technology Hossein Keramati & Seyed-Hassan Mirian-Hosseinabadi - 2015 - Elsevier
Mixed constraints for test input generation-An initial exploration Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering Shadi Abdul Khalek & Vidya Priyadarshini Narayanan & Sarfraz Khurshid - 2011
TestEra: A tool for testing Java programs using alloy specifications Proceedings of the 2011 26th IEEE/ACM international conference on automated software engineering Shadi Abdul Khalek & Guowei Yang & Lingming Zhang et al. - 2011
A Symbolic Execution Algorithm for Constraint-Based Testing of Database Programs arXiv preprint arXiv:1501.05821 Michaël Marcozzi & Wim Vanhoof & Jean-Luc Hainaut - 2015
A relational symbolic execution algorithm for constraint-based testing of database programs Source Code Analysis and Manipulation (SCAM), 2013 IEEE 13th International Working Conference on Michaël Marcozzi & Wim Vanhoof & J-L Hainaut - 2013
Test input generation for database programs using relational constraints Proceedings of the Fifth International Workshop on Testing Database Systems Michaël Marcozzi & Wim Vanhoof & Jean-Luc Hainaut - 2012
A 5-step hunt for faults in Java implementations of algebraic specifications Software Testing, Verification and Validation Workshops (ICSTW), 2013 IEEE Sixth International Conference on Isabel Nunes & Filipe Luıs - 2013
TacoFlow: optimizing sat program verification using dataflow analysis Software & Systems Modeling Bruno Cuervo Parrino & Juan Pablo Galeotti & Diego Garbervetsky et al. - 2014 - Springer
EQ: Checking the implementation of equality in Java Software Maintenance (ICSM), 2011 27th IEEE International Conference on Chandan Raj Rupakheti & Daqing Hou - 2011
Testing a Data-Intensive System with Generated Data Interactions Advanced Information Systems Engineering Sagar Sen & Arnaud Gotlieb - 2013
AUnit-a testing framework for alloy   Allison Sullivan - 2014
Towards a test automation framework for alloy Proceedings of the 2014 International SPIN Symposium on Model Checking of Software Allison Sullivan & Razieh Nokhbeh Zaeem & Sarfraz Khurshid et al. - 2014
PARADIGM-COV: A multimensional test coverage analysis tool Information Systems and Technologies (CISTI), 2014 9th Iberian Conference on Liliana Vilela & Ana CR Paiva - 2014
Specification-based test repair using a lightweight formal method FM 2012: Formal Methods Guowei Yang & Sarfraz Khurshid & Miryung Kim - 2012 - Springer
Automation of Model-Based Testing through Model Transformations Testing: Academic and Industrial …, 2009 - EG Aydal…
Automated SQL query generation for systematic testing of database engines … of the IEEE/ACM international conference …, 2010 - S Abdul Khalek…
Putting formal specifications under the magnifying glass: Model-based testing for validation … Testing Verification and …, 2009 - EG Aydal, RF Paige, M Utting…
Pairwise testing for software product lines: comparison of two approaches Software Quality …, 2011 - Springer G Perrouin, S Oster, S Sen, J Klein, B Baudry…
Pairwise testing of dynamic composite services Proceeding of the 6th …, 2011 - A Kattepur, S Sen, B Baudry, A Benveniste…
Systematic Testing of Database Engines Using a Relational Constraint Solver Software Testing, Verification and …, 2011 - SA Khalek…
Test data generation for web application using a UML class diagram with OCL constraints Innovations in Systems …, 2011 - Springer S Fujiwara, K Munakata, Y Maeda…
Relational Constraint Driven Test Case Synthesis for Web Applications Arxiv preprint arXiv:1009.3713, 2010 - X Fu

Configuration and Reconfiguration, Data Structure Repair

Indirect dependencies in dynamic reconfiguration of component-based systems Software Engineering and Service Science (ICSESS), 2014 5th IEEE International Conference on Mohammad Charaf Eddin & Zoubir Mammeri - 2014
Synthesis of Configuration Change Procedure Using Model Finder IEICE TRANSACTIONS on Information and Systems Shinji Kikuchi & Satoshi Tsuchiya & Kunihiko Hiraishi - 2013 - The Institute of Electronics, Information and Communication Engineers
On the simplicity of synthesizing linked data structure operations ACM SIGPLAN Notices Darya Kurilova & Derek Rayside - 2013
Data model property inference and repair Proceedings of the 2013 International Symposium on Software Testing and Analysis Jaideep Nijjar & Tevfik Bultan - 2013
FORS: Separating Configuration From Formal Specification   C Peters - 2014
History-aware data structure repair using SAT Tools and Algorithms for the Construction and Analysis of Systems Razieh Nokhbeh Zaeem & Divya Gopinath & Sarfraz Khurshid et al. - 2012 - Springer
Reliable dynamic reconfigurations in a reflective component model Component-Based Software …, 2010 - Springer M Leger, T Ledoux…
Configuration procedure synthesis for complex systems using model finder Engineering of Complex Computer …, 2010 S Kikuchi…
Security Domain Model and Implementation Modeling 2008 - M Auguston, A Shaffer
Contract-Based Data Structure Repair Using Alloy ECOOP 2010-Object-Oriented …, 2010 - Springer R Nokhbeh Zaeem…
Supporting change propagation in the evolution of enterprise architectures Enterprise Distributed Object …, 2010 HK Dam, LS Le… - g
Formal Logic Based Configuration Modeling and Verification for Dynamic Component Systems MOPAS 2011, The Second …, 2011 - Z Theisz, G Batori…
A formal approach to software synthesis for architectural platforms 33rd International Conference on Software Engineering, 2011 H Bagheri
Network configuration management via model finding Proceedings of the 19th conference on Large …, 2005 - S Narain


Model to specify real time system using Z and alloy languages: A comparative approach   Ashish Kumar Dwivedi & Santanu Ku Rath - 2012 - IET
Requirement progression: deriving specifications through problem diagrams   Joeri Peters - 2014
Generating Alloy Specification: From Textual User Requirements Written in Natural Language   Kiramat Rahman & Shabaz Ahmed Khan Ghayure - 2012 - LAP Lambert Academic Publishing
Requirements modeling in SEAM: The example of a car crash management system Comparing Requirements Modeling Approaches Workshop (CMA@ RE), 2013 International Alain Wegmann & Biljana Bajic-Bizumic & Arash Golnam et al. - 2013
Safety process improvement with POSE and Alloy Improvements in System Safety, 2008 - Springer D Mannering, JG Hall…