Case Study Applications
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…, 2008 |
| 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 |
Auctions
| 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… |
Security
| 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 - users.ece.utexas.edu | |
| 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 - cs.bu.edu | |
| A Lightweight Formal Analysis of a Multicast Key Management Scheme | IFIP Lecture Notes in Computer Science (LNCS), 2011 - dl.ifip.org | D Jackson… |
| Security Domain Model and Implementation Modeling | M Auguston, A Shaffer - 2008 | |
| Formal Models of a Least Privilege Separation Kernel in Alloy | M Auguston, TE Levin… - 2008 | |
| Toward a security domain model for static analysis and verification of information systems | 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 | Apurva Kumar - 2012 - IBM Research India | |
| Rigorous Analysis of UML Access Control Policy Models | W Sun, R France… - Policies for Distributed Systems and …, 2011 - ieeexplore.ieee.org | |
| 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 - dl.acm.org | H Hu… |
| Verification of policy-based self-managed cell interactions using alloy | Filho, E Lupu, M Sloman… - … and Networks, 2009. …, 2009 - ieeexplore.ieee.org | A Schaeffe |
| Ensuring spatio-temporal access control for real-world applications | Proceedings of the 14th …, 2009 - dl.acm.org | M Toahchoodee, I Ray, K Anastasakis… |
| Formal verification of OAuth 2.0 using Alloy framework | … Systems and Network …, 2011 - ieeexplore.ieee.org | 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 - pages.usherbrooke.ca | D Power, A Simpson… |
| New Approach for Testing the Correctness of Access Control Policies | 2009 - dspace.nitrkl.ac.in | 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 - cs.uwaterloo.ca | K Bak, K Czarnecki… |
| Detecting dependences and interactions in feature-oriented design | … (ISSRE), 2010 IEEE …, 2010 - ieeexplore.ieee.org | S Apel, W Scholz, C Lengauer… |
| Variability modeling and qos analysis of web services orchestrations | Web Services (ICWS), …, 2010 - ieeexplore.ieee.org | 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 - dl.acm.org | 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 - di.uminho.pt | MA Ferreira… |
| Verifying Intel flash file system core specification | … in VDM: Proceedings of the Fourth …, 2008 - cs.ncl.ac.uk | 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 - journal.ub.tu-berlin.de | A Bucchiarone… |
| A formal specification of the Fractal component model in Alloy | 2008 - hal.inria.fr | 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 - soa.fbk.eu | 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… |
Refactoring
| 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 - toritama.cin.ufpe.br | R Gheyi… |
| Toward a Formal Evaluation of Refactorings | Formal Methods …, 2008 - shemesh.larc.nasa.gov | J Paul, N Kuzmina, R Gamboa… |
| Formal model-driven program refactoring | Proceedings of the Theory and practice …, 2008 - dl.acm.org | 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 - mirrorservice.org | CR Rupakheti… |
| A Security Domain Model for Static Analysis and Verification of Software Programs | Proceedings of the 20th …, 2008 - alloy.mit.edu | AB Shaffer, M Auguston, C Irvine… |
| Analyzing Ruby on Rails Data Models using Alloy | GSWC 2010, 2010 - gswc.cs.ucsb.edu | J Nijjar… |
| Analysis of invariants for efficient bounded verification | Proceedings of the 19th …, 2010 - dl.acm.org | 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 - thinkmind.org | Z Theisz, G Batori… |
| An Abstraction-Oriented, Path-Based Approach for Analyzing Object Equality in Java | Reverse Engineering (WCRE), 2010 …, 2010 - ieeexplore.ieee.org | CR Rupakheti… |
Databases
| 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 - ieeexplore.ieee.org | 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 |
| Counterexamples to correctness of the Chord ring-maintenance protocol | 2010 - research.att.com | P Zave |
| Why the Chord ring-maintenance protocol is not correct | 2011 - research.att.com | P Zave |
| Lightweight Modeling of Network Protocols in Alloy | 2009 - public.research.att.com | P Zave |
| Compositional binding in network domains | International Symposium on Formal Methods, 2006 - public.research.att.com | 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 - ieeexplore.ieee.org | EG Aydal… |
| Automated SQL query generation for systematic testing of database engines | … of the IEEE/ACM international conference …, 2010 - dl.acm.org | S Abdul Khalek… |
| Evaluation of Automated Design Testing using Alloy | Software Engineering Research …, 2007 - caribou.iisg.agh.edu.pl | J Andersson… |
| Putting formal specifications under the magnifying glass: Model-based testing for validation | … Testing Verification and …, 2009 - ieeexplore.ieee.org | 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 - irisa.fr | A Kattepur, S Sen, B Baudry, A Benveniste… |
| Systematic Testing of Database Engines Using a Relational Constraint Solver | Software Testing, Verification and …, 2011 - ieeexplore.ieee.org | 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 - arxiv.org | X Fu |
| Pairwise testing for software product lines: comparison of two approaches | Software Quality …, 2011 - Springer | G Perrouin, S Oster, S Sen, J Klein, B Baudry… |
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 - 205.155.65.42 | 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 - thinkmind.org | 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 - dl.acm.org | S Narain |
Requirements
| 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… |