Practical Specification Techniques for Control-Oriented Systems. - Pamela Zave; Daniel Jackson 001 (IFIP Congress, 1989)

Aspect: An Economical Bug-Detector. - Daniel Jackson 001 (ICSE, 1991)

Abstract Analysis with Aspect. - Daniel Jackson 001 (ISSTA, 1993)

Abstract Model Checking of Infinite Specifications. - Daniel Jackson 001 (FME, 1994)

Semantic Diff: A Tool for Summarizing the Effects of Modifications. - Daniel Jackson 001; David A. Ladd (ICSM, 1994)

Abstraction mechanisms for pictorial slicing. - Daniel Jackson 001; Eugene J. Rollins (WPC, 1994)

A New Model of Program Dependences for Reverse Engineering. - Daniel Jackson 001; Eugene J. Rollins (SIGSOFT FSE, 1994)

The CMU Master of Software Engineering Core Curriculum. - David Garlan; Alan W. Brown; Daniel Jackson 001; James E. Tomayko; Jeannette M. Wing (CSEE, 1995)

Aspect: Detecting Bugs with Abstract Dependences. - Daniel Jackson 001 (ACM Trans. Softw. Eng. Methodol., 1995)

Structuring Z Specifications with Views - Daniel Jackson 001 (ACM Trans. Softw. Eng. Methodol., 1995)

Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector. - Daniel Jackson 001; Craig Damon (ISSTA, 1996)

Faster Checking of Software Specifications by Eliminating Isomorphs. - Daniel Jackson 001; Somesh Jha; Craig Damon (POPL, 1996)

Checking Relational Specifications With Binary Decision Diagrams. - Craig Damon; Daniel Jackson 001; Somesh Jha (SIGSOFT FSE, 1996)

Efficient Search as a Means of Executing Specifications. - Craig Damon; Daniel Jackson 001 (TACAS, 1996)

An Invitation to Formal Methods. - Jonathan P. Bowen; Ricky W. Butler; David L. Dill; Robert L. Glass; David Gries; Anthony Hall; Michael G. Hinchey; C. Michael Holloway; Daniel Jackson 001; Cliff B. Jones; Michael J. Lutz; David Lorge Parnas; et al. (Computer, 1996)

Problem decomposition for reuse. - Daniel Jackson 001; Michael Jackson 001 (Softw. Eng. J., 1996)

Do You Really Need Formal Requirements/Requirements Need Form, Maybe Formality (Point-Counterpoint). - Brian Lawrence; Daniel Jackson 001 (IEEE Softw., 1996)

Lackwit: A Program Understanding Tool Based on Type Inference. - Robert O'Callahan; Daniel Jackson 001 (ICSE, 1997)

An Intermedicate Design Language and Its Analysis. - Daniel Jackson 001 (SIGSOFT FSE, 1998)

Isomorph-Free Model Enumeration: A New Method for Checking Relational Specifications. - Daniel Jackson 001; Somesh Jha; Craig Damon (ACM Trans. Program. Lang. Syst., 1998)

Lightweight Extraction of Object Models from Bytecode. - Daniel Jackson 001; Allison Waingold (ICSE, 1999)

Guest Editorial. - Rance Cleaveland; Daniel Jackson 001 (Autom. Softw. Eng., 1999)

A Nitpick Analysis of Mobile IPv6. - Daniel Jackson 001; Yu-Chung Ng; Jeannette M. Wing (Formal Aspects Comput., 1999)

Software analysis: a roadmap: a roadmap. - Daniel Jackson 001; Martin C. Rinard (ICSE - Future of SE Track, 2000)

Alcoa: the alloy constraint analyzer. - Daniel Jackson 001; Ian Schechter; Ilya Shlyakhter (ICSE, 2000)

Finding bugs with a constraint solver. - Daniel Jackson 001; Mandana Vaziri (ISSTA, 2000)

Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer. - Sarfraz Khurshid; Daniel Jackson 001 (ASE, 2000)

Enforcing Design Constraints with Object Logic. - Daniel Jackson 001 (SAS, 2000)

Automating first-order relational logic. - Daniel Jackson 001 (SIGSOFT FSE, 2000)

COM revisited: tool-assisted modelling of an architectural framework. - Daniel Jackson 001; Kevin J. Sullivan (SIGSOFT FSE, 2000)

Some Shortcomings of OCL, the Object Constraint Language of UML. - Mandana Vaziri; Daniel Jackson 001 (TOOLS (34), 2000)

Redesigning Air Traffic Control: An Exercise in Software Design. - Daniel Jackson 001; John Chapin (IEEE Softw., 2000)

Lightweight Formal Methods. - Daniel Jackson 001 (FME, 2001)

A micromodularity mechanism. - Daniel Jackson 001; Ilya Shlyakhter; Manu Sridharan (ESEC / SIGSOFT FSE, 2001)

Lightweight Analysis of Object Interactions. - Daniel Jackson 001; Alan D. Fekete (TACS, 2001)

An analyzable annotation language. - Sarfraz Khurshid; Darko Marinov; Daniel Jackson 001 (OOPSLA, 2002)

Module Dependences in Software Design. - Daniel Jackson 001 (RISSEF, 2002)

Alloy: A New Technology for Software Modelling. - Daniel Jackson 001 (TACAS, 2002)

Alloy: a lightweight object modelling notation. - Daniel Jackson 001 (ACM Trans. Softw. Eng. Methodol., 2002)

A Lightweight Formal Analysis of a Multicast Key Management Scheme. - Mana Taghdiri; Daniel Jackson 001 (FORTE, 2003)

Debugging Overconstrained Declarative Models Using Unsatisfiable Cores. - Ilya Shlyakhter; Robert Seater; Daniel Jackson 001; Manu Sridharan; Mana Taghdiri (ASE, 2003)

Critical Feature Analysis of a Radiotherapy Machine. - Andrew Rae; Daniel Jackson 001; Prasad Ramanan; Jay Flanz; Didier Leyman (SAFECOMP, 2003)

A Case for Efficient Solution Enumeration. - Sarfraz Khurshid; Darko Marinov; Ilya Shlyakhter; Daniel Jackson 001 (SAT, 2003)

Checking Properties of Heap-Manipulating Procedures with a Constraint Solver. - Mandana Vaziri; Daniel Jackson 001 (TACAS, 2003)

Alloy: A Logical Modelling Language. - Daniel Jackson 001 (ZB, 2003)

Automating commutativity analysis at the design level. - Greg Dennis; Robert Seater; Derek Rayside; Daniel Jackson 001 (ISSTA, 2004)

Faster constraint solving with subtypes. - Jonathan Edwards; Daniel Jackson 001; Emina Torlak; Vincent Yeung (ISSTA, 2004)

Software assurance by bounded exhaustive testing. - Kevin J. Sullivan; Jinlin Yang; David Coppit; Sarfraz Khurshid; Daniel Jackson 001 (ISSTA, 2004)

A type system for object models. - Jonathan Edwards; Daniel Jackson 001; Emina Torlak (SIGSOFT FSE, 2004)

An analysis and visualization for revealing object sharing. - Derek Rayside; Lucy Mendel; Robert Seater; Daniel Jackson 001 (eTX, 2005)

Using dependency models to manage complex software architecture. - Neeraj Sangal; Ev Jordan; Vineet Sinha; Daniel Jackson 001 (OOPSLA, 2005)

Using dependency models to manage software architecture. - Neeraj Sangal; Ev Jordan; Vineet Sinha; Daniel Jackson 001 (OOPSLA Companion, 2005)

Dependable Software: An Oxymoron&. - Daniel Jackson 001 (RE, 2005)

Relational analysis of algebraic datatypes. - Viktor Kuncak; Daniel Jackson 001 (ESEC/SIGSOFT FSE, 2005)

Software Abstractions - Logic, Language, and Analysis. - Daniel Jackson 001 (MIT Press, 2006)

Idioms of Logical Modelling. - Daniel Jackson 001 (ICGT, 2006)

Symbolic model checking of declarative relational models. - Felix Sheng-Ho Chang; Daniel Jackson 001 (ICSE, 2006)

Problem frame transformations: deriving specifications from requirements. - Robert Seater; Daniel Jackson 001 (IWAAPF@ICSE, 2006)

Modular verification of code with SAT. - Greg Dennis; Felix Sheng-Ho Chang; Daniel Jackson 001 (ISSTA, 2006)

Requirement Progression in Problem Frames Applied to a Proton Therapy System. - Robert Seater; Daniel Jackson 001 (RE, 2006)

Separating Concerns in Requirements Analysis: An Example. - Daniel Jackson 001; Michael Jackson 001 (RODIN Book, 2006)

Lightweight extraction of syntactic specifications. - Mana Taghdiri; Robert Seater; Daniel Jackson 001 (SIGSOFT FSE, 2006)

Knowledge Flow Analysis for Security Protocols - Emina Torlak; Marten van Dijk; Blaise Gassend; Daniel Jackson 001; Srinivas Devadas (CoRR, 2006)

Kodkod: A Relational Model Finder. - Emina Torlak; Daniel Jackson 001 (TACAS, 2007)

Inferring specifications to detect errors in code. - Mana Taghdiri; Daniel Jackson 001 (Autom. Softw. Eng., 2007)

Automatic Visualization of Relational Logic Models. - Derek Rayside; Felix Sheng-Ho Chang; Greg Dennis; Robert Seater; Daniel Jackson 001 (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2007)

Requirement progression in problem frames: deriving specifications from requirements. - Robert Seater; Daniel Jackson 001; Rohit Gheyi (Requir. Eng., 2007)

Formal Modeling and Analysis of a Flash Filesystem in Alloy. - Eunsuk Kang; Daniel Jackson 001 (ABZ, 2008)

Finding Minimal Unsatisfiable Cores of Declarative Specifications. - Emina Torlak; Felix Sheng-Ho Chang; Daniel Jackson 001 (FM, 2008)

Hazards of Verification. - Daniel Jackson 001 (Haifa Verification Conference, 2008)

Bounded Verification of Voting Software. - Greg Dennis; Kuat Yessenov; Daniel Jackson 001 (VSTTE, 2008)

Equality and hashing for (almost) free: Generating implementations from abstraction functions. - Derek Rayside; Zev Benjamin; Rishabh Singh; Joseph P. Near; Aleksandar Milicevic; Daniel Jackson 001 (ICSE, 2009)

Agile specifications. - Derek Rayside; Aleksandar Milicevic; Kuat Yessenov; Greg Dennis; Daniel Jackson 001 (OOPSLA Companion, 2009)

A direct path to dependable software. - Daniel Jackson 001 (Commun. ACM, 2009)

Designing and Analyzing a Flash File System with Alloy. - Eunsuk Kang; Daniel Jackson 001 (Int. J. Softw. Informatics, 2009)

A Structure for Dependability Arguments. - Daniel Jackson 001; Eunsuk Kang (ASM, 2010)

An Imperative Extension to Alloy. - Joseph P. Near; Daniel Jackson 001 (ASM, 2010)

Patterns for building dependable systems with trusted bases. - Eunsuk Kang; Daniel Jackson 001 (PLoP, 2010)

Dependability Arguments with Trusted Bases. - Eunsuk Kang; Daniel Jackson 001 (RE, 2010)

Separation of concerns for dependable software design. - Daniel Jackson 001; Eunsuk Kang (FoSER, 2010)

Unifying execution of imperative and declarative code. - Aleksandar Milicevic; Derek Rayside; Kuat Yessenov; Daniel Jackson 001 (ICSE, 2011)

A lightweight code analysis and its role in evaluation of a dependability case. - Joseph P. Near; Aleksandar Milicevic; Eunsuk Kang; Daniel Jackson 001 (ICSE, 2011)

Preventing Arithmetic Overflows in Alloy. - Aleksandar Milicevic; Daniel Jackson 001 (ABZ, 2012)

Synthesizing iterators from abstraction functions. - Derek Rayside; Vajih Montaghami; Francesca Leung; Albert Yuen; Kevin Xu; Daniel Jackson 001 (GPCE, 2012)

Rubicon: bounded verification of web applications. - Joseph P. Near; Daniel Jackson 001 (SIGSOFT FSE, 2012)

Model-based, event-driven programming paradigm for interactive web applications. - Aleksandar Milicevic; Daniel Jackson 001; Milos Gligoric 001; Darko Marinov (Onward!, 2013)

What's wrong with git?: a conceptual design analysis. - Santiago Perez De Rosso; Daniel Jackson 001 (Onward!, 2013)

αRby - An Embedding of Alloy in Ruby. - Aleksandar Milicevic; Ido Efrati; Daniel Jackson 001 (ABZ, 2014)

Adaptive Defending Strategy for Smart Grid Attacks. - Jianye Hao; Eunsuk Kang; Daniel Jackson 001; Jun Sun 001 (SEGS@CCS, 2014)

Derailer: interactive security analysis for web applications. - Joseph P. Near; Daniel Jackson 001 (ASE, 2014)

Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification. - Hamid Bagheri; Eunsuk Kang; Sam Malek; Daniel Jackson 001 (FM, 2015)

Alloy*: A General-Purpose Higher-Order Relational Constraint Solver. - Aleksandar Milicevic; Joseph P. Near; Eunsuk Kang; Daniel Jackson 001 (ICSE (1), 2015)

Towards a theory of conceptual design for software. - Daniel Jackson 001 (Onward!, 2015)

Programming with enumerable sets of structures. - Ivan Kuraj; Viktor Kuncak; Daniel Jackson 001 (OOPSLA, 2015)

Model-based security analysis of a water treatment system. - Eunsuk Kang; Sridhar Adepu; Daniel Jackson 001; Aditya P. Mathur (SEsCPS@ICSE, 2016)

Finding security bugs in web applications using a catalog of access control patterns. - Joseph P. Near; Daniel Jackson 001 (ICSE, 2016)

Exploring the role of sequential computation in distributed systems: motivating a programming paradigm shift. - Ivan Kuraj; Daniel Jackson 001 (Onward!, 2016)

Object spreadsheets: a new computational model for end-user development of data-centric web applications. - Matt McCutchen; Shachar Itzhaky; Daniel Jackson 001 (Onward!, 2016)

Purposes, concepts, misfits, and a redesign of git. - Santiago Perez De Rosso; Daniel Jackson 001 (OOPSLA, 2016)

Designing minimal effective normative systems with the help of lightweight formal methods. - Jianye Hao; Eunsuk Kang; Jun Sun 001; Daniel Jackson 001 (SIGSOFT FSE, 2016)

Correct or usable? the limits of traditional verification (impact paper award). - Daniel Jackson 001; Mandana Vaziri (SIGSOFT FSE, 2016)

Multi-representational security analysis. - Eunsuk Kang; Aleksandar Milicevic; Daniel Jackson 001 (SIGSOFT FSE, 2016)

A formal approach for detection of security flaws in the android permission system. - Hamid Bagheri; Eunsuk Kang; Sam Malek; Daniel Jackson 001 (Formal Aspects Comput., 2018)

Declarative assembly of web applications from predefined concepts. - Santiago Perez De Rosso; Daniel Jackson 001; Maryam Archie; Czarina Lao; Barry A. McNamara III (Onward!, 2019)

Alloy: a language and tool for exploring software designs. - Daniel Jackson 001 (Commun. ACM, 2019)

Demystifying dependence. - James Koppel; Daniel Jackson 001 (Onward!, 2020)

End-user software customization by direct manipulation of tabular data. - Geoffrey Litt; Daniel Jackson 001; Tyler Millis; Jessica Ayeley Quaye (Onward!, 2020)

Wildcard: spreadsheet-driven customization of web applications. - Geoffrey Litt; Daniel Jackson 001 (Programming, 2020)

Towards End-User Web Scraping for Customization. - Kapaya Katongo; Geoffrey Litt; Daniel Jackson 001 (Programming, 2021)

Certified Control: An Architecture for Verifiable Safety of Autonomous Vehicles. - Daniel Jackson 001; Valerie Richmond; Mike Wang; Jeff Chow; Uriel Guajardo; Soonho Kong; Sergio Campos; Geoffrey Litt; Nikos Aréchiga (CoRR, 2021)

Merge what you can, fork what you can't: managing data integrity in local-first software. - Nicholas Schiefer; Geoffrey Litt; Daniel Jackson 001 (PaPoC@EuroSys, 2022)

Concept Design Moves. - Daniel Jackson 001 (NFM, 2022)

Concept-Centric Software Development: An Experience Report. - Peter A. Wilczynski; Taylor Gregoire-Wright; Daniel Jackson 001 (Onward!, 2023)

Riffle: Reactive Relational State for Local-First Applications. - Geoffrey Litt; Nicholas Schiefer; Johannes Schickling; Daniel Jackson 001 (UIST, 2023)

Concept-centric Software Development. - Peter A. Wilczynski; Taylor Gregoire-Wright; Daniel Jackson 001 (CoRR, 2023)

Bluefish: A Relational Grammar of Graphics. - Josh Pollock; Catherine Mei; Grace Huang; Daniel Jackson 001; Arvind Satyanarayan (CoRR, 2023)

Beyond Dark Patterns: A Concept-Based Framework for Software Design Ethics. - Evan Caragay; Katherine Xiong; Jonathan Zong; Daniel Jackson 001 (CoRR, 2023)

Beyond Dark Patterns: A Concept-Based Framework for Ethical Software Design. - Evan Caragay; Katherine Xiong; Jonathan Zong; Daniel Jackson 001 (CHI, 2024)

Keynote Lecture. - Daniel Jackson 001 (ENASE, 2024)

Bluefish: Composing Diagrams with Declarative Relations. - Josh Pollock; Catherine Mei; Grace Huang; Elliot Evans; Daniel Jackson 001; Arvind Satyanarayan (UIST, 2024)

A Concept-Oriented Approach to Software Development. - Daniel Jackson 001 (The Practice of Formal Methods (I), 2024)