var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https://groups.csail.mit.edu/sdg/sdgpub.bib&simplegroups=1&group0=year&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https://groups.csail.mit.edu/sdg/sdgpub.bib&simplegroups=1&group0=year&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https://groups.csail.mit.edu/sdg/sdgpub.bib&simplegroups=1&group0=year&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
  2. \n
  3. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
  4. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2023\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Beyond Dark Patterns: A Concept-Based Framework for Software Design Ethics.\n \n \n \n \n\n\n \n Caragay, E.; Xiong, K.; Zong, J.; and Jackson, D.\n\n\n \n\n\n\n 2023.\n \n\n\n\n
\n\n\n\n \n \n \"Beyond paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@misc{caragay2023dark,\n      title={Beyond Dark Patterns: A Concept-Based Framework for Software Design Ethics}, \n      author={Evan Caragay and Katherine Xiong and Jonathan Zong and Daniel Jackson},\n      year={2023},\n      eprint={2310.02432},\n      archivePrefix={arXiv},\n      primaryClass={cs.HC},\n      url_paper={pubs/2023/dark-concepts-23.pdf}\n}\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Concept Centric Software Development: An Experience Report.\n \n \n \n \n\n\n \n Wilczynski, P.; Gregoire-Wright, T.; and Jackson, D.\n\n\n \n\n\n\n In Onward!, ACM SIGPLAN Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH 2023), October 2023. \n \n\n\n\n
\n\n\n\n \n \n \"Concept paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Wilczynski_Gregoire-Wright_Jackson_2023, place={Lisbon, Portugal}, title={Concept Centric Software Development: An Experience Report}, booktitle={Onward!, ACM SIGPLAN Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH 2023)}, author={Wilczynski, Peter and Gregoire-Wright, Taylor and Jackson, Daniel}, year={2023}, month={October}, url_paper={pubs/2023/concepts-onward-23.pdf}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Riffle: Reactive Relational State for Local-First Applications.\n \n \n \n \n\n\n \n Litt, G.; Schiefer, N.; Schickling, J.; and Jackson, D.\n\n\n \n\n\n\n In ACM Symposium on User Interface Software and Technology (UIST), October 2023. \n \n\n\n\n
\n\n\n\n \n \n \"Riffle: paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Litt_Schiefer_Schickling_Jackson_2023, place={San Francisco, CA}, title={Riffle: Reactive Relational State for Local-First Applications}, booktitle={ACM Symposium on User Interface Software and Technology (UIST)}, author={Litt, Geoffrey and Schiefer, Nicholas and Schickling, Johannes and Jackson, Daniel}, year={2023}, month={October}, doi = {10.1145/3586183.3606801}, isbn = {979-8-4007-0132-0/23/10}, url_paper={pubs/2023/riffle-uist-23.pdf}}\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Language Model Agents Enable Semi-Formal Programming.\n \n \n \n \n\n\n \n Pollock, J.; Satyanarayan, A.; and Jackson, D.\n\n\n \n\n\n\n In The Ninth Workshop on Live Programming (LIVE 2023), October 2023. \n \n\n\n\n
\n\n\n\n \n \n \"Language paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Pollock_Satyanarayan_Jackson_2023, place={San Francisco, CA}, title={Language Model Agents Enable Semi-Formal Programming}, booktitle={The Ninth Workshop on Live Programming (LIVE 2023)}, author={Pollock, Josh and Satyanarayan, Arvind and Jackson, Daniel}, year={2023}, month={October}, url_paper={pubs/2023/lang-model-live-23.pdf}}\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Building Personal Software with Reactive Databases.\n \n \n \n \n\n\n \n Litt, G.\n\n\n \n\n\n\n Ph.D. Thesis, Massachusetts Institute of Technology, September 2023.\n \n\n\n\n
\n\n\n\n \n \n \"Building paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@phdthesis{Litt_PhD_2023, title={Building Personal Software with Reactive Databases}, author={Litt, Geoffrey}, school={Massachusetts Institute of Technology}, year={2023}, month={September}, url_paper={pubs/2023/litt_phd_thesis.pdf}}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Building data-centric apps with a reactive relational database.\n \n \n \n \n\n\n \n Litt, G.; Schiefer, N.; Schickling, J.; and Jackson, D.\n\n\n \n\n\n\n Programming Local-First Software Workshop 2022. June 2022.\n \n\n\n\n
\n\n\n\n \n \n \"Building paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{Litt_Schiefer_Schickling_Jackson_2022, title={Building data-centric apps with a reactive relational database}, journal={Programming Local-First Software Workshop 2022}, author={Litt, Geoffrey and Schiefer, Nicholas and Schickling, Johannes and Jackson, Daniel}, year={2022}, month={June}, url_paper={https://riffle.systems/essays/prelude}}\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Concept Design Moves.\n \n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n In NASA Formal Methods 2022, May 2022. \n \n\n\n\n
\n\n\n\n \n \n \"Concept paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Jackson_2022, place={Pasadena, CA}, title={Concept Design Moves}, booktitle={NASA Formal Methods 2022}, author={Jackson, Daniel}, year={2022}, month={May}, url_paper={pubs/2022/nfm-jackson.pdf}}\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Peritext: A CRDT for Collaborative Rich Text Editing.\n \n \n \n \n\n\n \n Litt, G.; Lim, S.; Kleppmann, M.; and van Hardenberg, P.\n\n\n \n\n\n\n Proceedings of the ACM on Human-Computer Interaction, 6(CSCW2). November 2022.\n Article 531\n\n\n\n
\n\n\n\n \n \n \"Peritext: paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 14 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{Litt_Lim_Kleppmann_VanHardenberg_2022, title={Peritext: A CRDT for Collaborative Rich Text Editing}, DOI={10.1145/3555644}, journal={Proceedings of the ACM on Human-Computer Interaction}, author={Litt, Geoffrey and Lim, Sarah and Kleppmann, Martin and van Hardenberg, Peter}, year={2022}, month={November}, url_paper={pubs/2022/Peritext_PACM_HCI_2022.pdf}, volume={6}, number={CSCW2}, note={Article 531}}\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Merge What You Can, Fork What You Can’t: Managing Data Integrity in Local-First Software.\n \n \n \n \n\n\n \n Schiefer, N.; Litt, G.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 9th Workshop on Principles and Practice of Consistency for Distributed Data, Apr 2022. \n \n\n\n\n
\n\n\n\n \n \n \"Merge paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 6 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Schiefer_Litt_Jackson_2022, place={Rennes, France}, title={Merge What You Can, Fork What You Can’t: Managing Data Integrity in Local-First Software}, booktitle={Proceedings of the 9th Workshop on Principles and Practice of Consistency for Distributed Data}, author={Schiefer, Nicholas and Litt, Geoffrey and Jackson, Daniel}, year={2022}, month={Apr}, url_paper={pubs/2022/Merge_What_You_Can_PaPoC_2022.pdf}, DOI={10.1145/3517209.3524041}}\n\n 
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Joker: A Unified Interaction Model For Web Customization.\n \n \n \n \n\n\n \n Katongo, K.; Litt, G.; Jin, K.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of LIVE 2021, the Seventh Workshop on Live Programming, Oct 2021. \n \n\n\n\n
\n\n\n\n \n \n \"Joker: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Katongo_Litt_Jin_Jackson_2021, place={Virtual, USA}, title={Joker: A Unified Interaction Model For Web Customization}, booktitle={Proceedings of LIVE 2021, the Seventh Workshop on Live Programming}, author={Katongo, Kapaya and Litt, Geoffrey and Jin, Kathryn and Jackson, Daniel}, year={2021}, month={Oct}, url_paper={pubs/2021/Joker_LIVE_2021.pdf}}\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Certified Perception for Autonomous Cars.\n \n \n \n \n\n\n \n Guajardo, U.; Bryan, A.; Arechiga, N.; Campos, S.; Chow, J.; Jackson, D.; Kong, S.; Litt, G.; and Pollock, J.\n\n\n \n\n\n\n In 6th Workshop on Monitoring and Testing of Cyber-Physical Systems, May 2021. \n \n\n\n\n
\n\n\n\n \n \n \"Certified paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Guajardo_Bryan_Arechiga_Campos_Chow_Jackson_Kong_Litt_Pollock_2021, place={Virtual}, title={Certified Perception for Autonomous Cars}, author={Guajardo, Uriel and Bryan, Annie and Arechiga, Nikos and Campos, Sergio and Chow, Jeff and Jackson, Daniel and Kong, Soonho and Litt, Geoffrey and Pollock, Josh}, year={2021}, month={May}, url_paper={pubs/2021/Guajardo et al. - 2021 - Certified Perception for Autonomous Cars.pdf}, booktitle={6th Workshop on Monitoring and Testing of Cyber-Physical Systems} }\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards End-user Web Scraping For Customization.\n \n \n \n \n\n\n \n Katongo, K.; Litt, G.; and Jackson, D.\n\n\n \n\n\n\n In Companion Proceedings of the 5th International Conference on the Art, Science, and Engineering of Programming, Mar 2021. \n \n\n\n\n
\n\n\n\n \n \n \"Towards paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Katongo_Litt_Jackson_2021, place={Virtual, UK}, title={Towards End-user Web Scraping For Customization}, booktitle={Companion Proceedings of the 5th International Conference on the Art, Science, and Engineering of Programming}, author={Katongo, Kapaya and Litt, Geoffrey and Jackson, Daniel}, year={2021}, month={Mar}, url_paper={pubs/2021/Katongo et al. - 2021 - Towards End-user Web Scraping For Customization.pdf}}\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Certified Control: An Architecture for Verifiable Safety of Autonomous Vehicles.\n \n \n \n \n\n\n \n Jackson, D.; Richmond, V.; Wang, M.; Chow, J.; Guajardo, U.; Kong, S.; Campos, S.; Litt, G.; and Arechiga, N.\n\n\n \n\n\n\n arXiv:2104.06178 [cs, eess]. Mar 2021.\n arXiv: 2104.06178\n\n\n\n
\n\n\n\n \n \n \"CertifiedPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{Jackson_Richmond_Wang_Chow_Guajardo_Kong_Campos_Litt_Arechiga_2021, title={Certified Control: An Architecture for Verifiable Safety of Autonomous Vehicles}, url={http://arxiv.org/abs/2104.06178}, note={arXiv: 2104.06178}, journal={arXiv:2104.06178 [cs, eess]}, author={Jackson, Daniel and Richmond, Valerie and Wang, Mike and Chow, Jeff and Guajardo, Uriel and Kong, Soonho and Campos, Sergio and Litt, Geoffrey and Arechiga, Nikos}, year={2021}, month={Mar} }\n\n 
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Demystifying Dependence.\n \n \n \n \n\n\n \n Koppel, J.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, pages 48–64, Nov 2020. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Demystifying paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Koppel_Jackson_2020,\n  place={Virtual USA},\n  title={Demystifying Dependence},\n  ISBN={978-1-4503-8178-9},\n  url_paper={pubs/2020/demystifying_dependence_published.pdf},\n  DOI={10.1145/3426428.3426916},\n  booktitle={Proceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software},\n  publisher={ACM},\n  author={Koppel, James and Jackson, Daniel},\n  year={2020},\n  month={Nov},\n  pages={48–64} }\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n End-user Software Customization by Direct Manipulation of Tabular Data.\n \n \n \n \n\n\n \n Litt, G.; Jackson, D.; Millis, T.; and Quaye, J.\n\n\n \n\n\n\n In Proceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, pages 18–33, Nov 2020. ACM\n \n\n\n\n
\n\n\n\n \n \n \"End-user paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 11 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Litt_Jackson_Millis_Quaye_2020,\n  place={Virtual USA},\n  title={End-user Software Customization by Direct Manipulation of Tabular Data},\n  ISBN={978-1-4503-8178-9},\n  url_paper={pubs/2020/Wildcard-Onward-published.pdf},\n  DOI={10.1145/3426428.3426914},\n  booktitle={Proceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software},\n  publisher={ACM},\n  author={Litt, Geoffrey and Jackson, Daniel and Millis, Tyler and Quaye, Jessica},\n  year={2020},\n  month={Nov},\n  pages={18–33} }\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Wildcard: Spreadsheet-Driven Customization of Web Applications.\n \n \n \n \n\n\n \n Litt, G.; and Jackson, D.\n\n\n \n\n\n\n In Convivial Computing Salon 2020, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"Wildcard: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 18 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Litt-Wildcard-Convivial,\n author = {Geoffrey Litt and Daniel Jackson},\n title = {Wildcard: Spreadsheet-Driven Customization of Web Applications},\n booktitle = {Convivial Computing Salon 2020},\n year = {2020},\n url_paper = {https://www.geoffreylitt.com/wildcard/salon2020/}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n WIP: Finding Bugs Automatically in Smart Contracts with Parameterized Specifications.\n \n \n \n \n\n\n \n Bernardi, T.; Dor, N.; Fedotov, A.; Grossman, S.; Immerman, N.; Jackson, D.; Nutz, A.; Oppenheim, L.; Rinetzky, N.; Sagiv, M.; Taube, M.; and Wilcox, J. R.\n\n\n \n\n\n\n In 4th Stanford Blockchain Conference 2020, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"WIP: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{SBC2020-smart-contract-bugs,\n author = {Thomas Bernardi and Nurit Dor and Anastasia Fedotov and Shelly Grossman and Neil Immerman and Daniel Jackson and Alexander Nutz and Lior Oppenheim and Noam Rinetzky and Mooly Sagiv and Marcelo Taube and James R. Wilcox},\n title = {WIP: Finding Bugs Automatically in Smart Contracts with Parameterized Specifications},\n booktitle = {4th Stanford Blockchain Conference 2020},\n year = {2020},\n url_paper = {pubs/2020/sbc2020.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Certified Control: A New Safety Architecture for Autonomous Vehicles.\n \n \n \n \n\n\n \n Chow, J.; Richmond, V.; Wang, M.; Guajardo, U.; Jackson, D.; Arechiga, N.; Litt, G.; Kong, S.; and Campos, S.\n\n\n \n\n\n\n In Submitted for publication, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"Certified paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{certified-control-2020,\n author = {Jeff Chow and Valerie Richmond and Mike Wang and Uriel Guajardo and Daniel Jackson and Nikos Arechiga and Geoffrey Litt and Soonho Kong and Sergio Campos},\n title = {Certified Control: A New Safety Architecture for Autonomous Vehicles},\n booktitle = {Submitted for publication},\n year = {2020},\n url_paper = {pubs/2020/certified-control.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Declarative Assembly of Web Applications from Predefined Concepts.\n \n \n \n \n\n\n \n Perez De Rosso, S.; Jackson, D.; Archie, M.; Lao, C.; and McNamara III, B. A.\n\n\n \n\n\n\n In Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, of Onward! 2019, pages 79–93, New York, NY, USA, 2019. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Declarative paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{PerezDeRosso:2019:DAW:3359591.3359728,\n author = {Perez De Rosso, Santiago and Jackson, Daniel and Archie, Maryam and Lao, Czarina and McNamara III, Barry A.},\n title = {Declarative Assembly of Web Applications from Predefined Concepts},\n booktitle = {Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software},\n series = {Onward! 2019},\n year = {2019},\n isbn = {978-1-4503-6995-4},\n location = {Athens, Greece},\n pages = {79--93},\n numpages = {15},\n doi = {10.1145/3359591.3359728},\n acmid = {3359728},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {application development, concepts, design, modularity, software design, web applications},\n url_paper = {pubs/2019/onward19.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Alloy: A Language and Tool for Exploring Software Designs.\n \n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n Commun. ACM, 62(9): 66–76. August 2019.\n \n\n\n\n
\n\n\n\n \n \n \"Alloy: paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{Jackson:2019:ALT:3358415.3338843,\n author = {Jackson, Daniel},\n title = {Alloy: A Language and Tool for Exploring Software Designs},\n journal = {Commun. ACM},\n issue_date = {September 2019},\n volume = {62},\n number = {9},\n month = aug,\n year = {2019},\n issn = {0001-0782},\n pages = {66--76},\n numpages = {11},\n doi = {10.1145/3338843},\n acmid = {3338843},\n publisher = {ACM},\n address = {New York, NY, USA},\n url_paper = {pubs/2019/alloy-cacm-18-feb-22-2019.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Certified Control for Self-Driving Cars.\n \n \n \n \n\n\n \n Jackson, D.; DeCastro, J.; Kong, S.; Koutentakis, D.; Leong, A. F. P.; Solar-Lezama, A.; Wang, M.; and Zhang, X.\n\n\n \n\n\n\n In DARS 2019: 4th Workshop On The Design And Analysis Of Robust Systems, 2019. \n \n\n\n\n
\n\n\n\n \n \n \"Certified paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{jackson-dars,\n  author = {Jackson, Daniel and DeCastro, Jonathan and Kong, Soonho and Koutentakis, Dimitrios and Leong, Angela Feng Ping and Solar-Lezama, Armando and Wang, Mike and Zhang, Xin},\n  title = {Certified Control for Self-Driving Cars},\n  booktitle = {DARS 2019: 4th Workshop On The Design And Analysis Of Robust Systems},\n  year = 2019,\n  url_paper = {pubs/2019/dars-final.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Espalier: a structured spreadsheet tool for end-user development of organizational applications.\n \n \n \n \n\n\n \n McCutchen, M.; Itzhaky, S.; Jackson, D.; and Jarvis, W.\n\n\n \n\n\n\n In LIVE 2018, 2018. \n \n\n\n\n
\n\n\n\n \n \n \"Espalier:Paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{espalier-live2018,\n author = {McCutchen, Matt and Itzhaky, Shachar and Jackson, Daniel and Jarvis, Willow},\n title = {Espalier: a structured spreadsheet tool for end-user development of organizational applications},\n booktitle = {LIVE 2018},\n year = 2018,\n url = {pubs/2018/espalier-live-2018-video.mp4}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Designing Minimal Effective Normative Systems with the Help of Lightweight Formal Methods.\n \n \n \n \n\n\n \n Hao, J.; Kang, E.; Sun, J.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, of FSE 2016, pages 50–60, New York, NY, USA, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Designing paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{Hao:2016:DME:2950290.2950307,\n author = {Hao, Jianye and Kang, Eunsuk and Sun, Jun and Jackson, Daniel},\n title = {Designing Minimal Effective Normative Systems with the Help of Lightweight Formal Methods},\n booktitle = {Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering},\n series = {FSE 2016},\n year = {2016},\n isbn = {978-1-4503-4218-6},\n location = {Seattle, WA, USA},\n pages = {50--60},\n numpages = {11},\n url_paper = {pubs/2016/norms-fse16.pdf},\n doi = {10.1145/2950290.2950307},\n acmid = {2950307},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {Lightweight formal methods, Minimal effective, Norm Synthesis}\n}\n\n% Downloaded from https://eskang.github.io/papers/poirot-fse16.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Multi-representational Security Analysis.\n \n \n \n \n\n\n \n Kang, E.; Milicevic, A.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, of FSE 2016, pages 181–192, New York, NY, USA, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Multi-representational paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{Kang:2016:MSA:2950290.2950356,\n author = {Kang, Eunsuk and Milicevic, Aleksandar and Jackson, Daniel},\n title = {Multi-representational Security Analysis},\n booktitle = {Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering},\n series = {FSE 2016},\n year = {2016},\n isbn = {978-1-4503-4218-6},\n location = {Seattle, WA, USA},\n pages = {181--192},\n numpages = {12},\n url_paper = {pubs/2016/poirot-fse16.pdf},\n doi = {10.1145/2950290.2950356},\n acmid = {2950356},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {Security, composition, modeling, representation, verification},\n}\n\n% Downloaded from http://people.csail.mit.edu/sperezde/oopsla16.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Purposes, Concepts, Misfits, and a Redesign of Git.\n \n \n \n \n\n\n \n De Rosso, S. P.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, of OOPSLA 2016, pages 292–310, New York, NY, USA, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Purposes, paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{DeRosso:2016:PCM:2983990.2984018,\n author = {De Rosso, Santiago Perez and Jackson, Daniel},\n title = {Purposes, Concepts, Misfits, and a Redesign of Git},\n booktitle = {Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},\n series = {OOPSLA 2016},\n year = {2016},\n isbn = {978-1-4503-4444-9},\n location = {Amsterdam, Netherlands},\n pages = {292--310},\n numpages = {19},\n url_paper = {pubs/2016/gitless-oopsla16.pdf},\n doi = {10.1145/2983990.2984018},\n acmid = {2984018},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {Git, concept design, concepts, design, software design, usability, version control},\n}\n\n% Downloaded from https://sdg.csail.mit.edu/projects/objsheets/objsheets-onward2016.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Object Spreadsheets: A New Computational Model for End-user Development of Data-centric Web Applications.\n \n \n \n \n\n\n \n McCutchen, M.; Itzhaky, S.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 2016 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, of Onward! 2016, pages 112–127, New York, NY, USA, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Object paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@inproceedings{McCutchen:2016:OSN:2986012.2986018,\n author = {McCutchen, Matt and Itzhaky, Shachar and Jackson, Daniel},\n title = {Object Spreadsheets: A New Computational Model for End-user Development of Data-centric Web Applications},\n booktitle = {Proceedings of the 2016 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software},\n series = {Onward! 2016},\n year = {2016},\n isbn = {978-1-4503-4076-2},\n location = {Amsterdam, Netherlands},\n pages = {112--127},\n numpages = {16},\n url_paper = {pubs/2016/objsheets-onward2016.pdf},\n doi = {10.1145/2986012.2986018},\n acmid = {2986018},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {End-user development},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Exploring the Role of Sequential Computation in Distributed Systems: Motivating a Programming Paradigm Shift.\n \n \n \n \n\n\n \n Kuraj, I.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 2016 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, of Onward! 2016, pages 145–164, New York, NY, USA, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Exploring paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{Kuraj:2016:ERS:2986012.2986015,\n author = {Kuraj, Ivan and Jackson, Daniel},\n title = {Exploring the Role of Sequential Computation in Distributed Systems: Motivating a Programming Paradigm Shift},\n booktitle = {Proceedings of the 2016 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software},\n series = {Onward! 2016},\n year = {2016},\n isbn = {978-1-4503-4076-2},\n location = {Amsterdam, Netherlands},\n pages = {145--164},\n numpages = {20},\n url_paper = {pubs/2016/distributed-programming-onward2016.pdf},\n doi = {10.1145/2986012.2986015},\n acmid = {2986015},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {declarative programming, distributed, programming model, reactive, separation of concerns, software synthesis},\n}\n\n% Downloaded from https://dspace.mit.edu/openaccess-disseminate/1721.1/102281 by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Finding Security Bugs in Web Applications Using a Catalog of Access Control Patterns.\n \n \n \n \n\n\n \n Near, J. P.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 38th International Conference on Software Engineering, of ICSE '16, pages 947–958, New York, NY, USA, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Finding paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{Near:2016:FSB:2884781.2884836,\n author = {Near, Joseph P. and Jackson, Daniel},\n title = {Finding Security Bugs in Web Applications Using a Catalog of Access Control Patterns},\n booktitle = {Proceedings of the 38th International Conference on Software Engineering},\n series = {ICSE '16},\n year = {2016},\n isbn = {978-1-4503-3900-1},\n location = {Austin, Texas},\n pages = {947--958},\n numpages = {12},\n url_paper = {pubs/2016/access-control-patterns-icse2016.pdf},\n doi = {10.1145/2884781.2884836},\n acmid = {2884836},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {access control, bug finding, web application security},\n}\n\n% Downloaded from https://sdg.csail.mit.edu/projects/objsheets/mccutchen-ms-thesis-objsheets.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Object Spreadsheets: an end-user development tool for web applications backed by entity-relationship data.\n \n \n \n \n\n\n \n McCutchen, R. M.\n\n\n \n\n\n\n Master's thesis, Massachusetts Institute of Technology, June 2016.\n \n\n\n\n
\n\n\n\n \n \n \"Object paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@mastersthesis{McCutchen-ms-objsheets,\n title = {Object Spreadsheets: an end-user development tool for web applications backed by entity-relationship data},\n author = {Richard Matthew McCutchen},\n school = {Massachusetts Institute of Technology},\n year = 2016,\n month = June,\n url_paper = {pubs/2016/mccutchen-ms-thesis-objsheets.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Model-based security analysis of a water treatment system.\n \n \n \n \n\n\n \n Kang, E.; Adepu, S.; Jackson, D.; and Mathur, A. P.\n\n\n \n\n\n\n In 2nd International Workshop on Software Engineering for Smart Cyber-Physical Systems, 2016. \n \n\n\n\n
\n\n\n\n \n \n \"Model-based paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{ICSE16-CPS,\n  author    = {Eunsuk Kang and Sridhar Adepu and Daniel Jackson and\n               Aditya P. Mathur},\n  title     = {Model-based security analysis of a water treatment system},\n  booktitle = {2nd International Workshop on Software Engineering for Smart Cyber-Physical Systems},\n  year      = {2016},\nurl_paper={pubs/2016/icse16-cps.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n The Same-Origin Policy.\n \n \n \n \n\n\n \n Kang, E.; Perez De Rosso, S.; and Jackson, D.\n\n\n \n\n\n\n In DiBernardo, M., editor(s), The Architecture of Open Source Applications, Volume 4: 500 Lines or Less. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{aosa-same-origin-policy,\n author = {Kang, Eunsuk and Perez De Rosso, Santiago and Jackson, Daniel},\n title = {The Same-Origin Policy},\n booktitle = {The Architecture of Open Source Applications, Volume 4: 500 Lines or Less},\n year = 2015,\n editor = {Michael DiBernardo},\n url = {http://aosabook.org/en/500L/the-same-origin-policy.html}\n}\n\n% Downloaded from https://eskang.github.io/papers/norms-fse16.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Programming with Enumerable Sets of Structures.\n \n \n \n \n\n\n \n Kuraj, I.; Kuncak, V.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, of OOPSLA 2015, pages 37–56, New York, NY, USA, 2015. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Programming paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{Kuraj:2015:PES:2814270.2814323,\n author = {Kuraj, Ivan and Kuncak, Viktor and Jackson, Daniel},\n title = {Programming with Enumerable Sets of Structures},\n booktitle = {Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},\n series = {OOPSLA 2015},\n year = {2015},\n isbn = {978-1-4503-3689-5},\n location = {Pittsburgh, PA, USA},\n pages = {37--56},\n numpages = {20},\n url_paper = {pubs/2015/enumeration-oopsla2015.pdf},\n doi = {10.1145/2814270.2814323},\n acmid = {2814323},\n publisher = {ACM},\n address = {New York, NY, USA},\n keywords = {DSL, Dependent enumeration, SciFe, algebra, data generation, exhaustive testing, invariant, lazy evaluation, pairing function, program inversion, random testing},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Towards a Theory of Conceptual Design for Software.\n \n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n In Onward! Essays, 2015. \n \n\n\n\n
\n\n\n\n \n \n \"Towards paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{dnj-towards,\n author = {Daniel Jackson},\n title = {Towards a Theory of Conceptual Design for Software},\n booktitle = {Onward! Essays},\n year = {2015},\n url_paper={pubs/2015/concept-essay.pdf},\n}\n\n% Downloaded from https://eskang.github.io/papers/android-fm15.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification.\n \n \n \n \n\n\n \n Bagheri, H.; Kang, E.; Malek, S.; and Jackson, D.\n\n\n \n\n\n\n In 20th International Symposium on Formal Methods (FM), 2015. \n \n\n\n\n
\n\n\n\n \n \n \"Detection paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/fm/BagheriKMJ15,\n  author    = {Hamid Bagheri and\n               Eunsuk Kang and\n               Sam Malek and\n               Daniel Jackson},\n  title     = {Detection of Design Flaws in the Android Permission Protocol Through\n               Bounded Verification},\n  booktitle = {20th International Symposium on Formal Methods (FM)},\n  year      = {2015},\n  url_paper = {pubs/2015/android-fm15.pdf}\n}\n\n% Downloaded from http://dspace.mit.edu/bitstream/handle/1721.1/89157/MIT-CSAIL-TR-2014-018.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Alloy*: A General-Purpose Higher-Order Relational Constraint Solver (ACM SIGSOFT Distinguished Paper Award).\n \n \n \n \n\n\n \n Milicevic, A.; Near, J. P.; Kang, E.; and Jackson, D.\n\n\n \n\n\n\n In 37th IEEE/ACM International Conference on Software Engineering (ICSE), 2015. \n \n\n\n\n
\n\n\n\n \n \n \"Alloy*: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/MilicevicNKJ15,\n  author    = {Aleksandar Milicevic and\n               Joseph P. Near and\n               Eunsuk Kang and\n               Daniel Jackson},\n  title     = {Alloy*: {A} General-Purpose Higher-Order Relational Constraint Solver (ACM SIGSOFT Distinguished Paper Award)},\n  booktitle = {37th {IEEE/ACM} International Conference on Software Engineering (ICSE)},\n  year      = {2015},\n  url_paper = {pubs/2015/icse15-alloystar.pdf}\n}\n\n% Link originally went to http://www.gregdennis.com/alloy_mscs_2013.pdf, which is broken.\n% Downloaded from http://homes.cs.washington.edu/~emina/pubs/alloy.mscs13.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Alloy*: A Higher-Order Relational Constraint Solver.\n \n \n \n \n\n\n \n Milicevic, A.; Near, J. P.; Kang, E.; and Jackson, D.\n\n\n \n\n\n\n Technical Report MIT-CSAIL-TR-2014-018, CSAIL, MIT, 2014.\n \n\n\n\n
\n\n\n\n \n \n \"Alloy*: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@techreport{hola-tr,\n  author    = {Aleksandar Milicevic and\n               Joseph P. Near and\n               Eunsuk Kang and\n               Daniel Jackson},\n    title     = {Alloy*: A Higher-Order Relational Constraint Solver},\n    institution = "CSAIL, MIT",\n    number   = "MIT-CSAIL-TR-2014-018",\n    year      = {2014},\nurl_paper={pubs/2014/alloystar-tr-2014.pdf}\n}\n\n% Downloaded from http://alloy.mit.edu/alloy/hola/downloads/icse15-alloystar.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Derailer: Interactive Security Analysis for Web Applications.\n \n \n \n \n\n\n \n Near, J. P; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2014. IEEE/ACM\n \n\n\n\n
\n\n\n\n \n \n \"Derailer: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{near2014derailer,\n  title={Derailer: Interactive Security Analysis for Web Applications},\n  author={Near, Joseph P and Jackson, Daniel},\n  booktitle={Proceedings of the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE)},\n  year={2014},\n  organization={IEEE/ACM},\nurl_paper={pubs/2014/derailer-ase14.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n aRby—An Embedding of Alloy in Ruby.\n \n \n \n \n\n\n \n Milicevic, A. E.; and Jackson, D.\n\n\n \n\n\n\n In Abstract State Machines, Alloy, B, VDM, and Z, of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2014.\n \n\n\n\n
\n\n\n\n \n \n \"aRby—An paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@incollection{arby,\n  year={2014},\n  booktitle={Abstract State Machines, Alloy, B, VDM, and Z},\n  series={Lecture Notes in Computer Science},\n  title={aRby---An Embedding of Alloy in Ruby},\n  publisher={Springer Berlin Heidelberg},\n  author={Milicevic, Aleksandar Erfrati, Ido and Jackson, Daniel},\nurl_paper={pubs/2014/abz14-arby.pdf}\n}\n\n% Downloaded from http://people.csail.mit.edu/aleks/website/papers/onward13-red.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Applications and extensions of Alloy: past, present and future.\n \n \n \n \n\n\n \n Torlak, E.; Taghdiri, M.; Dennis, G.; and Near, J. P.\n\n\n \n\n\n\n Mathematical Structures in Computer Science, 23(4): 915-933. 2013.\n \n\n\n\n
\n\n\n\n \n \n \"Applications paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/mscs/TorlakTDN13,\n  author    = {Emina Torlak and\n               Mana Taghdiri and\n               Greg Dennis and\n               Joseph P. Near},\n  title     = {Applications and extensions of Alloy: past, present and\n               future},\n  journal   = {Mathematical Structures in Computer Science},\n  volume    = {23},\n  number    = {4},\n  year      = {2013},\n  pages     = {915-933},\n  url_paper = {pubs/2013/alloy.mscs13.pdf}\n}\n\n% Downloaded from http://people.csail.mit.edu/jnear/papers/ase14.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Model-based, event-driven programming paradigm for interactive web applications.\n \n \n \n \n\n\n \n Milicevic, A.; Jackson, D.; Gligoric, M.; and Marinov, D.\n\n\n \n\n\n\n In Onward!, pages 17-36, 2013. \n \n\n\n\n
\n\n\n\n \n \n \"Model-based, paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/oopsla/MilicevicJGM13,\n  author    = {Aleksandar Milicevic and\n               Daniel Jackson and\n               Milos Gligoric and\n               Darko Marinov},\n  title     = {Model-based, event-driven programming paradigm for interactive\n               web applications},\n  booktitle = {Onward!},\n  year      = {2013},\n  pages     = {17-36},\nurl_paper = {pubs/2013/onward13-red.pdf}\n}\n\n% Downloaded from http://dspace.mit.edu/bitstream/handle/1721.1/79826/MIT-CSAIL-TR-2013-020.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Conceptual Design of Software: A Research Agenda.\n \n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n Technical Report MIT-CSAIL-TR-2013-020, CSAIL, MIT, August 2013.\n \n\n\n\n
\n\n\n\n \n \n \"Conceptual paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@techreport{dnj-tr-conceptual-design,\n    author    = "Daniel Jackson",\n    title     = "Conceptual Design of Software: A Research Agenda",\n    institution = "CSAIL, MIT",\n    number   = "MIT-CSAIL-TR-2013-020",\n    year      = "2013",\n    month    = "August",\nurl_paper={pubs/2013/conceptual-research-agenda-2013.pdf}\n}\n\n% Downloaded from http://people.csail.mit.edu/sperezde/onward13.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n What's wrong with git? a conceptual design analysis.\n \n \n \n \n\n\n \n Perez De Rosso, S.; and Jackson, D.\n\n\n \n\n\n\n In Onward!, pages 37-52, 2013. \n \n\n\n\n
\n\n\n\n \n \n \"What's paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/oopsla/RossoJ13,\n  author    = {Santiago Perez{ }De{ }Rosso and\n               Daniel Jackson},\n  title     = {What's wrong with git? a conceptual design analysis},\n  booktitle = {Onward!},\n  year      = {2013},\n  pages     = {37-52},\nurl_paper={pubs/2013/git-conceptual-onward13.pdf}\n}\n\n% Downloaded from http://people.csail.mit.edu/aleks/website/papers/splash12-jen.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2012\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Program extrapolation with jennisys.\n \n \n \n \n\n\n \n Leino, K. R. M.; and Milicevic, A.\n\n\n \n\n\n\n In OOPSLA, pages 411-430, 2012. \n \n\n\n\n
\n\n\n\n \n \n \"Program paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/oopsla/LeinoM12,\n  author    = {K. Rustan M. Leino and\n               Aleksandar Milicevic},\n  title     = {Program extrapolation with jennisys},\n  booktitle = {OOPSLA},\n  year      = {2012},\n  pages     = {411-430},\nurl_paper={pubs/2012/splash12-jen.pdf}\n}\n\n% Downloaded from http://people.csail.mit.edu/jnear/papers/fse12.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Rubicon: bounded verification of web applications.\n \n \n \n \n\n\n \n Near, J. P.; and Jackson, D.\n\n\n \n\n\n\n In SIGSOFT FSE, pages 60, 2012. \n \n\n\n\n
\n\n\n\n \n \n \"Rubicon: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/NearJ12,\n  author    = {Joseph P. Near and\n               Daniel Jackson},\n  title     = {Rubicon: bounded verification of web applications},\n  booktitle = {SIGSOFT FSE},\n  year      = {2012},\n  pages     = {60},\nurl_paper={pubs/2012/rubicon-fse12.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Preventing Arithmetic Overflows in Alloy.\n \n \n \n \n\n\n \n Milicevic, A.; and Jackson, D.\n\n\n \n\n\n\n In Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, pages 108-121, 2012. \n \n\n\n\n
\n\n\n\n \n \n \"Preventing paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/asm/MilicevicJ12,\n  author    = {Aleksandar Milicevic and\n               Daniel Jackson},\n  title     = {Preventing Arithmetic Overflows in Alloy},\n  booktitle = {Abstract State Machines, Alloy, B, VDM, and Z - Third International\n               Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings},\n  year      = {2012},\n  pages     = {108-121},\nurl_paper={pubs/2012/abz12-overflow.pdf},\n}\n\n% Downloaded from https://ece.uwaterloo.ca/~drayside/gpce12-synthesizing-iterators.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesizing iterators from abstraction functions.\n \n \n \n \n\n\n \n Rayside, D.; Montaghami, V.; Leung, F.; Yuen, A.; Xu, K.; and Jackson, D.\n\n\n \n\n\n\n In Generative Programming and Component Engineering, GPCE'12, Dresden, Germany, September 26-28, 2012, pages 31-40, 2012. \n \n\n\n\n
\n\n\n\n \n \n \"Synthesizing paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/gpce/RaysideMLYXJ12,\n  author    = {Derek Rayside and\n               Vajih Montaghami and\n               Francesca Leung and\n               Albert Yuen and\n               Kevin Xu and\n               Daniel Jackson},\n  title     = {Synthesizing iterators from abstraction functions},\n  booktitle = {Generative Programming and Component Engineering, GPCE'12,\n               Dresden, Germany, September 26-28, 2012},\n  year      = {2012},\n  pages     = {31-40},\nurl_paper={pubs/2012/gpce12-synthesizing-iterators.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2011\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A lightweight code analysis and its role in evaluation of a dependability case.\n \n \n \n \n\n\n \n Near, J. P.; Milicevic, A.; Kang, E.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011, pages 31-40, 2011. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/NearMKJ11,\n  author    = {Joseph P. Near and\n               Aleksandar Milicevic and\n               Eunsuk Kang and\n               Daniel Jackson},\n  title     = {A lightweight code analysis and its role in evaluation of\n               a dependability case},\n  booktitle = {Proceedings of the 33rd International Conference on Software\n               Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May\n               21-28, 2011},\n  year      = {2011},\n  pages     = {31-40},\nurl_paper={pubs/2011/icse11-lightweight.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Unifying execution of imperative and declarative code.\n \n \n \n \n\n\n \n Milicevic, A.; Rayside, D.; Yessenov, K.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011, pages 511-520, 2011. \n \n\n\n\n
\n\n\n\n \n \n \"Unifying paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/MilicevicRYJ11,\n  author    = {Aleksandar Milicevic and\n               Derek Rayside and\n               Kuat Yessenov and\n               Daniel Jackson},\n  title     = {Unifying execution of imperative and declarative code},\n  booktitle = {Proceedings of the 33rd International Conference on Software\n               Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May\n               21-28, 2011},\n  year      = {2011},\n  pages     = {511-520},\nurl_paper={pubs/2011/icse11-squander.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2010\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n An Imperative Extension to Alloy.\n \n \n \n \n\n\n \n Near, J. P.; and Jackson, D.\n\n\n \n\n\n\n In Abstract State Machines, Alloy, B and Z, Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings, pages 118-131, 2010. \n \n\n\n\n
\n\n\n\n \n \n \"An paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/asm/NearJ10,\n  author    = {Joseph P. Near and\n               Daniel Jackson},\n  title     = {An Imperative Extension to Alloy},\n  booktitle = {Abstract State Machines, Alloy, B and Z, Second International\n               Conference, ABZ 2010, Orford, QC, Canada, February 22-25,\n               2010. Proceedings},\n  year      = {2010},\n  pages     = {118-131},\nurl_paper={pubs/2010/dynamic-alloy.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Dependability Arguments with Trusted Bases.\n \n \n \n \n\n\n \n Kang, E.; and Jackson, D.\n\n\n \n\n\n\n In RE 2010, 18th IEEE International Requirements Engineering Conference, Sydney, New South Wales, Australia, September 27 - October 1, 2010, pages 262-271, 2010. \n \n\n\n\n
\n\n\n\n \n \n \"Dependability paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/re/KangJ10,\n  author    = {Eunsuk Kang and\n               Daniel Jackson},\n  title     = {Dependability Arguments with Trusted Bases},\n  booktitle = {RE 2010, 18th IEEE International Requirements Engineering\n               Conference, Sydney, New South Wales, Australia, September\n               27 - October 1, 2010},\n  year      = {2010},\n  pages     = {262-271},\nurl_paper={pubs/2010/re10-kang-jackson.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Separation of concerns for dependable software design.\n \n \n \n \n\n\n \n Jackson, D.; and Kang, E.\n\n\n \n\n\n\n In Proceedings of the Workshop on Future of Software Engineering Research, FoSER 2010, Santa Fe, NM, USA, November 7-11, 2010, pages 173-176, 2010. \n \n\n\n\n
\n\n\n\n \n \n \"Separation paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/JacksonK10,\n  author    = {Daniel Jackson and\n               Eunsuk Kang},\n  title     = {Separation of concerns for dependable software design},\n  booktitle = {Proceedings of the Workshop on Future of Software Engineering\n               Research, FoSER 2010,\n               Santa Fe, NM, USA, November 7-11, 2010},\n  year      = {2010},\n  pages     = {173-176},\nurl_paper={pubs/2010/future-workshop-10.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2009\n \n \n (6)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Property-part diagrams: A dependence notation for software systems.\n \n \n \n \n\n\n \n Jackson, D.; and Kang, E.\n\n\n \n\n\n\n In ICSE Workshop: A Tribute to Michael Jackson, May 2009. \n \n\n\n\n
\n\n\n\n \n \n \"Property-part paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{Jackson_Kang_2009, place={Vancouver, BC}, title={Property-part diagrams: A dependence notation for software systems}, booktitle={ICSE Workshop: A Tribute to Michael Jackson}, author={Jackson, Daniel and Kang, Eunsuk}, year={2009}, month={May}, url_paper={pubs/2009/Jackson_Property part.pdf}}\n\n 
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Michael Jackson Design Technique: A study of the theory with applications.\n \n \n \n \n\n\n \n Hoare, C. A. R.\n\n\n \n\n\n\n In Jackson, D., editor(s), ICSE Workshop: A Tribute to Michael Jackson, 2009. \n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{jackson_JSP,\n  author    = {Charles Anthony Richard Hoare},\n  editor = {Daniel Jackson},\n  title     = {The Michael Jackson Design Technique: A study of the theory with applications.},\n  booktitle = {ICSE Workshop: A Tribute to Michael Jackson},\n  year      = {2009},\n  url_paper={pubs/2009/hoare-jsp-3-29-09.pdf}\n}\n\n% Downloaded from http://people.csail.mit.edu/aleks/website/papers/abz14-arby.pdf by Matt, 2017-03-06\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A direct path to dependable software.\n \n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n Commun. ACM, 52(4): 78-88. 2009.\n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/cacm/Jackson09,\n  author    = {Daniel Jackson},\n  title     = {A direct path to dependable software},\n  journal   = {Commun. ACM},\n  volume    = {52},\n  number    = {4},\n  year      = {2009},\n  pages     = {78-88},\nurl_paper={pubs/2009/dnj-cacm-4-09.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Designing and Analyzing a Flash File System with Alloy.\n \n \n \n \n\n\n \n Kang, E.; and Jackson, D.\n\n\n \n\n\n\n Int. J. Software and Informatics, 3(2-3): 129-148. 2009.\n \n\n\n\n
\n\n\n\n \n \n \"Designing paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/ijsi/KangJ09,\n  author    = {Eunsuk Kang and\n               Daniel Jackson},\n  title     = {Designing and Analyzing a Flash File System with Alloy},\n  journal   = {Int. J. Software and Informatics},\n  volume    = {3},\n  number    = {2-3},\n  year      = {2009},\n  pages     = {129-148},\n  url_paper={pubs/2009/ijsi09_flash.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Equality and hashing for (almost) free: Generating implementations from abstraction functions.\n \n \n \n \n\n\n \n Rayside, D.; Benjamin, Z.; Singh, R.; Near, J. P.; Milicevic, A.; and Jackson, D.\n\n\n \n\n\n\n In 31st International Conference on Software Engineering, ICSE 2009, May 16-24, 2009, Vancouver, Canada, Proceedings, pages 342-352, 2009. \n \n\n\n\n
\n\n\n\n \n \n \"Equality paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/RaysideBSNMJ09,\n  author    = {Derek Rayside and\n               Zev Benjamin and\n               Rishabh Singh and\n               Joseph P. Near and\n               Aleksandar Milicevic and\n               Daniel Jackson},\n  title     = {Equality and hashing for (almost) free: Generating implementations\n               from abstraction functions},\n  booktitle = {31st International Conference on Software Engineering, ICSE\n               2009, May 16-24, 2009, Vancouver, Canada, Proceedings},\n  year      = {2009},\n  pages     = {342-352},\n url_paper={pubs/2009/icse09-object-contract.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Agile specifications.\n \n \n \n \n\n\n \n Rayside, D.; Milicevic, A.; Yessenov, K.; Dennis, G.; and Jackson, D.\n\n\n \n\n\n\n In Companion to the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009, October 25-29, 2009, Orlando, Florida, USA, pages 999-1006, 2009. \n \n\n\n\n
\n\n\n\n \n \n \"Agile paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/oopsla/RaysideMYDJ09,\n  author    = {Derek Rayside and\n               Aleksandar Milicevic and\n               Kuat Yessenov and\n               Greg Dennis and\n               Daniel Jackson},\n  title     = {Agile specifications},\n  booktitle = {Companion to the 24th Annual ACM SIGPLAN Conference on Object-Oriented\n               Programming, Systems, Languages, and Applications, OOPSLA\n               2009, October 25-29, 2009, Orlando, Florida, USA},\n  year      = {2009},\n  pages     = {999-1006},\n   url_paper={pubs/2009/onward09-agile-specifications.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2008\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Formal Modeling and Analysis of a Flash Filesystem in Alloy.\n \n \n \n \n\n\n \n Kang, E.; and Jackson, D.\n\n\n \n\n\n\n In Abstract State Machines, B and Z, First International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings, pages 294-308, 2008. \n \n\n\n\n
\n\n\n\n \n \n \"Formal paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/asm/KangJ08,\n  author    = {Eunsuk Kang and\n               Daniel Jackson},\n  title     = {Formal Modeling and Analysis of a Flash Filesystem in Alloy},\n  booktitle = {Abstract State Machines, B and Z, First International Conference,\n               ABZ 2008, London, UK, September 16-18, 2008. Proceedings},\n  year      = {2008},\n  pages     = {294-308},\nurl_paper={pubs/2008/abz08_kang_jackson.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Finding Minimal Unsatisfiable Cores of Declarative Specifications.\n \n \n \n \n\n\n \n Torlak, E.; Chang, F. S.; and Jackson, D.\n\n\n \n\n\n\n In FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008, Proceedings, pages 326-341, 2008. \n \n\n\n\n
\n\n\n\n \n \n \"Finding paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/fm/TorlakCJ08,\n  author    = {Emina Torlak and\n               Felix Sheng-Ho Chang and\n               Daniel Jackson},\n  title     = {Finding Minimal Unsatisfiable Cores of Declarative Specifications},\n  booktitle = {FM 2008: Formal Methods, 15th International Symposium on\n               Formal Methods, Turku, Finland, May 26-30, 2008, Proceedings},\n  year      = {2008},\n  pages     = {326-341},\nurl_paper={pubs/2008/mincore-fm08.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Bounded Verification of Voting Software.\n \n \n \n \n\n\n \n Dennis, G.; Yessenov, K.; and Jackson, D.\n\n\n \n\n\n\n In Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings , pages 130-145, 2008. \n \n\n\n\n
\n\n\n\n \n \n \"Bounded paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/vstte/DennisYJ08,\n  author    = {Greg Dennis and\n               Kuat Yessenov and\n               Daniel Jackson},\n  title     = {Bounded Verification of Voting Software},\n  booktitle = {Verified Software: Theories, Tools, Experiments, Second\n               International Conference, VSTTE 2008, Toronto, Canada, October\n               6-9, 2008. Proceedings },\n  year      = {2008},\n  pages     = {130-145},\nurl_paper={pubs/2008/dennis-bounded.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2007\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Automatic Visualization of Relational Logic Models.\n \n \n \n \n\n\n \n Rayside, D.; Chang, F. S.; Dennis, G.; Seater, R.; and Jackson, D.\n\n\n \n\n\n\n ECEASST, 7. 2007.\n \n\n\n\n
\n\n\n\n \n \n \"Automatic paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/eceasst/RaysideCDSJ07,\n  author    = {Derek Rayside and\n               Felix Sheng-Ho Chang and\n               Greg Dennis and\n               Robert Seater and\n               Daniel Jackson},\n  title     = {Automatic Visualization of Relational Logic Models},\n  journal   = {ECEASST},\n  volume    = {7},\n  year      = {2007},\n url_paper={pubs/2007/alloy-led07.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Requirement progression in problem frames: deriving specifications from requirements.\n \n \n \n \n\n\n \n Seater, R.; Jackson, D.; and Gheyi, R.\n\n\n \n\n\n\n Requir. Eng., 12(2): 77-102. 2007.\n \n\n\n\n
\n\n\n\n \n \n \"Requirement paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/re/SeaterJG07,\n  author    = {Robert Seater and\n               Daniel Jackson and\n               Rohit Gheyi},\n  title     = {Requirement progression in problem frames: deriving specifications\n               from requirements},\n  journal   = {Requir. Eng.},\n  volume    = {12},\n  number    = {2},\n  year      = {2007},\n  pages     = {77-102},\n url_paper={pubs/2007/REJ.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Kodkod: A Relational Model Finder.\n \n \n \n \n\n\n \n Torlak, E.; and Jackson, D.\n\n\n \n\n\n\n In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, pages 632-647, 2007. \n \n\n\n\n
\n\n\n\n \n \n \"Kodkod: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/tacas/TorlakJ07,\n  author    = {Emina Torlak and\n               Daniel Jackson},\n  title     = {Kodkod: A Relational Model Finder},\n  booktitle = {Tools and Algorithms for the Construction and Analysis of\n               Systems, 13th International Conference, TACAS 2007, Held\n               as Part of the Joint European Conferences on Theory and\n               Practice of Software, ETAPS 2007 Braga, Portugal, March\n               24 - April 1, 2007, Proceedings},\n  year      = {2007},\n  pages     = {632-647},\nurl_paper={pubs/2007/tacas07-torlak-jackson.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2006\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Software Abstractions - Logic, Language, and Analysis.\n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n MIT Press, 2006.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@book{DBLP:books/daglib/0024034,\n  author    = {Daniel Jackson},\n  title     = {Software Abstractions - Logic, Language, and Analysis},\n  publisher = {MIT Press},\n  year      = {2006},\n  isbn      = {978-0-262-10114-1},\n  pages     = {I-XVI, 1-350},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Symbolic model checking of declarative relational models.\n \n \n \n \n\n\n \n Chang, F. S.; and Jackson, D.\n\n\n \n\n\n\n In 28th International Conference on Software Engineering (ICSE 2006), Shanghai, China, May 20-28, 2006, pages 312-320, 2006. \n \n\n\n\n
\n\n\n\n \n \n \"Symbolic paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/ChangJ06,\n  author    = {Felix Sheng-Ho Chang and\n               Daniel Jackson},\n  title     = {Symbolic model checking of declarative relational models},\n  booktitle = {28th International Conference on Software Engineering (ICSE\n               2006), Shanghai, China, May 20-28, 2006},\n  year      = {2006},\n  pages     = {312-320},\n url_paper={pubs/2006/chang-symbolic-decl.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Modular verification of code with SAT.\n \n \n \n\n\n \n Dennis, G.; Chang, F. S.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, July 17-20, 2006, pages 109-120, 2006. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/issta/DennisCJ06,\n  author    = {Greg Dennis and\n               Felix Sheng-Ho Chang and\n               Daniel Jackson},\n  title     = {Modular verification of code with SAT},\n  booktitle = {Proceedings of the ACM/SIGSOFT International Symposium on\n               Software Testing and Analysis, ISSTA 2006, Portland, Maine,\n               USA, July 17-20, 2006},\n  year      = {2006},\n  pages     = {109-120},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Requirement Progression in Problem Frames Applied to a Proton Therapy System.\n \n \n \n \n\n\n \n Seater, R.; and Jackson, D.\n\n\n \n\n\n\n In 14th IEEE International Conference on Requirements Engineering (RE 2006), 11-15 September 2006, Minneapolis/St.Paul, Minnesota, USA, pages 166-175, 2006. \n \n\n\n\n
\n\n\n\n \n \n \"Requirement paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/re/SeaterJ06,\n  author    = {Robert Seater and\n               Daniel Jackson},\n  title     = {Requirement Progression in Problem Frames Applied to a Proton\n               Therapy System},\n  booktitle = {14th IEEE International Conference on Requirements Engineering\n               (RE 2006), 11-15 September 2006, Minneapolis/St.Paul, Minnesota,\n               USA},\n  year      = {2006},\n  pages     = {166-175},\n url_paper={pubs/2006/RE06.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Separating Concerns in Requirements Analysis: An Example.\n \n \n \n \n\n\n \n Jackson, D.; and Jackson, M.\n\n\n \n\n\n\n In Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project], pages 210-225, 2006. \n \n\n\n\n
\n\n\n\n \n \n \"Separating paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/rodin/JacksonJ06,\n  author    = {Daniel Jackson and\n               Michael Jackson},\n  title     = {Separating Concerns in Requirements Analysis: An Example},\n  booktitle = {Rigorous Development of Complex Fault-Tolerant Systems [FP6\n               IST-511599 RODIN project]},\n  year      = {2006},\n  pages     = {210-225},\nurl_paper={pubs/2006/reft-06.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Lightweight extraction of syntactic specifications.\n \n \n \n \n\n\n \n Taghdiri, M.; Seater, R.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, Portland, Oregon, USA, November 5-11, 2006, pages 276-286, 2006. \n \n\n\n\n
\n\n\n\n \n \n \"Lightweight paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/TaghdiriSJ06,\n  author    = {Mana Taghdiri and\n               Robert Seater and\n               Daniel Jackson},\n  title     = {Lightweight extraction of syntactic specifications},\n  booktitle = {Proceedings of the 14th ACM SIGSOFT International Symposium\n               on Foundations of Software Engineering, FSE 2006, Portland,\n               Oregon, USA, November 5-11, 2006},\n  year      = {2006},\n  pages     = {276-286},\n url_paper={pubs/2006/FSE06.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Knowledge Flow Analysis for Security Protocols.\n \n \n \n\n\n \n Torlak, E.; van Dijk, M.; Gassend, B.; Jackson, D.; and Devadas, S.\n\n\n \n\n\n\n CoRR, abs/cs/0605109. 2006.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/corr/abs-cs-0605109,\n  author    = {Emina Torlak and\n               Marten van Dijk and\n               Blaise Gassend and\n               Daniel Jackson and\n               Srinivas Devadas},\n  title     = {Knowledge Flow Analysis for Security Protocols},\n  journal   = {CoRR},\n  volume    = {abs/cs/0605109},\n  year      = {2006},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2005\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Critical feature analysis of a radiotherapy machine.\n \n \n \n\n\n \n Rae, A.; Jackson, D.; Ramanan, P.; Flanz, J.; and Leyman, D.\n\n\n \n\n\n\n Rel. Eng. & Sys. Safety, 89(1): 48-56. 2005.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/ress/RaeJRFL05,\n  author    = {Andrew Rae and\n               Daniel Jackson and\n               Prasad Ramanan and\n               Jay Flanz and\n               Didier Leyman},\n  title     = {Critical feature analysis of a radiotherapy machine},\n  journal   = {Rel. Eng. {\\&} Sys. Safety},\n  volume    = {89},\n  number    = {1},\n  year      = {2005},\n  pages     = {48-56},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An analysis and visualization for revealing object sharing.\n \n \n \n\n\n \n Rayside, D.; Mendel, L.; Seater, R.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 2005 OOPSLA workshop on Eclipse Technology eXchange, ETX 2005, San Diego, California, USA, October 16-17, 2005, pages 11-15, 2005. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/eclipse/RaysideMSJ05,\n  author    = {Derek Rayside and\n               Lucy Mendel and\n               Robert Seater and\n               Daniel Jackson},\n  title     = {An analysis and visualization for revealing object sharing},\n  booktitle = {Proceedings of the 2005 OOPSLA workshop on Eclipse Technology\n               eXchange, ETX 2005, San Diego, California, USA, October\n               16-17, 2005},\n  year      = {2005},\n  pages     = {11-15},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Using dependency models to manage complex software architecture.\n \n \n \n \n\n\n \n Sangal, N.; Jordan, E.; Sinha, V.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA, pages 167-176, 2005. \n \n\n\n\n
\n\n\n\n \n \n \"Using paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/oopsla/SangalJSJ05,\n  author    = {Neeraj Sangal and\n               Ev Jordan and\n               Vineet Sinha and\n               Daniel Jackson},\n  title     = {Using dependency models to manage complex software architecture},\n  booktitle = {Proceedings of the 20th Annual ACM SIGPLAN Conference on\n               Object-Oriented Programming, Systems, Languages, and Applications,\n               OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA},\n  year      = {2005},\n  pages     = {167-176},\nurl_paper={pubs/2005/oopsla05-dsm.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Relational analysis of algebraic datatypes.\n \n \n \n \n\n\n \n Kuncak, V.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 10th European Software Engineering Conference, 2005, Lisbon, Portugal, September 5-9, 2005, pages 207-216, 2005. \n \n\n\n\n
\n\n\n\n \n \n \"Relational paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/KuncakJ05,\n  author    = {Viktor Kuncak and\n               Daniel Jackson},\n  title     = {Relational analysis of algebraic datatypes},\n  booktitle = {Proceedings of the 10th European Software Engineering\n                  Conference, 2005, Lisbon, Portugal, September 5-9,\n                  2005},\n  year      = {2005},\n  pages     = {207-216},\nurl_paper={pubs/2005/RelationalAnalysisDatatypes.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2004\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Software assurance by bounded exhaustive testing.\n \n \n \n\n\n \n Sullivan, K. J.; Yang, J.; Coppit, D.; Khurshid, S.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July 11-14, 2004, pages 133-142, 2004. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/issta/SullivanYCKJ04,\n  author    = {Kevin J. Sullivan and\n               Jinlin Yang and\n               David Coppit and\n               Sarfraz Khurshid and\n               Daniel Jackson},\n  title     = {Software assurance by bounded exhaustive testing},\n  booktitle = {Proceedings of the ACM/SIGSOFT International Symposium on\n               Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts,\n               USA, July 11-14, 2004},\n  year      = {2004},\n  pages     = {133-142},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automating commutativity analysis at the design level.\n \n \n \n \n\n\n \n Dennis, G.; Seater, R.; Rayside, D.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July 11-14, 2004, pages 165-174, 2004. \n \n\n\n\n
\n\n\n\n \n \n \"Automating paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/issta/DennisSRJ04,\n  author    = {Greg Dennis and\n               Robert Seater and\n               Derek Rayside and\n               Daniel Jackson},\n  title     = {Automating commutativity analysis at the design level},\n  booktitle = {Proceedings of the ACM/SIGSOFT International Symposium on\n               Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts,\n               USA, July 11-14, 2004},\n  year      = {2004},\n  pages     = {165-174},\nurl_paper={pubs/2004/proton.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Faster constraint solving with subtypes.\n \n \n \n \n\n\n \n Edwards, J.; Jackson, D.; Torlak, E.; and Yeung, V.\n\n\n \n\n\n\n In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July 11-14, 2004, pages 232-242, 2004. \n \n\n\n\n
\n\n\n\n \n \n \"Faster paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/issta/EdwardsJTY04,\n  author    = {Jonathan Edwards and\n               Daniel Jackson and\n               Emina Torlak and\n               Vincent Yeung},\n  title     = {Faster constraint solving with subtypes},\n  booktitle = {Proceedings of the ACM/SIGSOFT International Symposium on\n               Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts,\n               USA, July 11-14, 2004},\n  year      = {2004},\n  pages     = {232-242},\nurl_paper={pubs/2004/atom.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A type system for object models.\n \n \n \n \n\n\n \n Edwards, J.; Jackson, D.; and Torlak, E.\n\n\n \n\n\n\n In Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2004, Newport Beach, CA, USA, October 31 - November 6, 2004, pages 189-199, 2004. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/EdwardsJT04,\n  author    = {Jonathan Edwards and\n               Daniel Jackson and\n               Emina Torlak},\n  title     = {A type system for object models},\n  booktitle = {Proceedings of the 12th ACM SIGSOFT International Symposium\n               on Foundations of Software Engineering, 2004, Newport Beach,\n               CA, USA, October 31 - November 6, 2004},\n  year      = {2004},\n  pages     = {189-199},\n url_paper={pubs/2004/typeSystem.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2003\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Lightweight Formal Analysis of a Multicast Key Management Scheme.\n \n \n \n \n\n\n \n Taghdiri, M.; and Jackson, D.\n\n\n \n\n\n\n In Formal Techniques for Networked and Distributed Systems - FORTE 2003, 23rd IFIP WG 6.1 International Conference, Berlin, Germany, September 29 - October 2, 2003, Proceedings, pages 240-256, 2003. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/forte/TaghdiriJ03,\n  author    = {Mana Taghdiri and\n               Daniel Jackson},\n  title     = {A Lightweight Formal Analysis of a Multicast Key Management\n               Scheme},\n  booktitle = {Formal Techniques for Networked and Distributed Systems\n               - FORTE 2003, 23rd IFIP WG 6.1 International Conference,\n               Berlin, Germany, September 29 - October 2, 2003, Proceedings},\n  year      = {2003},\n  pages     = {240-256},\nurl_paper={pubs/2003/Forte03-taghdiri.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Debugging Overconstrained Declarative Models Using Unsatisfiable Cores.\n \n \n \n \n\n\n \n Shlyakhter, I.; Seater, R.; Jackson, D.; Sridharan, M.; and Taghdiri, M.\n\n\n \n\n\n\n In 18th IEEE International Conference on Automated Software Engineering (ASE 2003), 6-10 October 2003, Montreal, Canada, pages 94-105, 2003. \n \n\n\n\n
\n\n\n\n \n \n \"Debugging paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/kbse/ShlyakhterSJST03,\n  author    = {Ilya Shlyakhter and\n               Robert Seater and\n               Daniel Jackson and\n               Manu Sridharan and\n               Mana Taghdiri},\n  title     = {Debugging Overconstrained Declarative Models Using Unsatisfiable\n               Cores},\n  booktitle = {18th IEEE International Conference on Automated Software\n               Engineering (ASE 2003), 6-10 October 2003, Montreal, Canada},\n  year      = {2003},\n  pages     = {94-105},\nurl_paper={pubs/2003/ucore.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Critical Feature Analysis of a Radiotherapy Machine.\n \n \n \n \n\n\n \n Rae, A.; Jackson, D.; Ramanan, P.; Flanz, J.; and Leyman, D.\n\n\n \n\n\n\n In Computer Safety, Reliability, and Security, 22nd International Conference, SAFECOMP 2003, Edinburgh, UK, September 23-26, 2003, Proceedings, pages 221-234, 2003. \n \n\n\n\n
\n\n\n\n \n \n \"Critical paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/safecomp/RaeJRFL03,\n  author    = {Andrew Rae and\n               Daniel Jackson and\n               Prasad Ramanan and\n               Jay Flanz and\n               Didier Leyman},\n  title     = {Critical Feature Analysis of a Radiotherapy Machine},\n  booktitle = {Computer Safety, Reliability, and Security, 22nd International\n               Conference, SAFECOMP 2003, Edinburgh, UK, September 23-26,\n               2003, Proceedings},\n  year      = {2003},\n  pages     = {221-234},\nurl_paper={pubs/2003/safecomp-journal.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Case for Efficient Solution Enumeration.\n \n \n \n \n\n\n \n Khurshid, S.; Marinov, D.; Shlyakhter, I.; and Jackson, D.\n\n\n \n\n\n\n In Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, pages 272-286, 2003. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sat/KhurshidMSJ03,\n  author    = {Sarfraz Khurshid and\n               Darko Marinov and\n               Ilya Shlyakhter and\n               Daniel Jackson},\n  title     = {A Case for Efficient Solution Enumeration},\n  booktitle = {Theory and Applications of Satisfiability Testing, 6th International\n               Conference, SAT 2003. Santa Margherita Ligure, Italy, May\n               5-8, 2003 Selected Revised Papers},\n  year      = {2003},\n  pages     = {272-286},\nurl_paper={pubs/2003/testera_SAT03.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Checking Properties of Heap-Manipulating Procedures with a Constraint Solver.\n \n \n \n \n\n\n \n Vaziri, M.; and Jackson, D.\n\n\n \n\n\n\n In Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Proceedings, pages 505-520, 2003. \n \n\n\n\n
\n\n\n\n \n \n \"Checking paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/tacas/VaziriJ03,\n  author    = {Mandana Vaziri and\n               Daniel Jackson},\n  title     = {Checking Properties of Heap-Manipulating Procedures with\n               a Constraint Solver},\n  booktitle = {Tools and Algorithms for the Construction and Analysis\n                  of Systems, 9th International Conference, TACAS\n                  2003, Proceedings},\n  year      = {2003},\n  pages     = {505-520},\nurl_paper={pubs/2003/checkingHMPs.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2002\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Alloy: a lightweight object modelling notation.\n \n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n ACM Trans. Softw. Eng. Methodol., 11(2): 256-290. 2002.\n \n\n\n\n
\n\n\n\n \n \n \"Alloy: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/tosem/Jackson02,\n  author    = {Daniel Jackson},\n  title     = {Alloy: a lightweight object modelling notation},\n  journal   = {ACM Trans. Softw. Eng. Methodol.},\n  volume    = {11},\n  number    = {2},\n  year      = {2002},\n  pages     = {256-290},\nurl_paper={pubs/2002/alloy-journal.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n An analyzable annotation language.\n \n \n \n \n\n\n \n Khurshid, S.; Marinov, D.; and Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, Seattle, Washington, USA, November 4-8, 2002, pages 231-245, 2002. \n \n\n\n\n
\n\n\n\n \n \n \"An paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/oopsla/KhurshidMJ02,\n  author    = {Sarfraz Khurshid and\n               Darko Marinov and\n               Daniel Jackson},\n  title     = {An analyzable annotation language},\n  booktitle = {Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented\n               Programming Systems, Languages and Applications, OOPSLA\n               2002, Seattle, Washington, USA, November 4-8, 2002},\n  year      = {2002},\n  pages     = {231-245},\n url_paper={pubs/2002/AAL.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Module Dependences in Software Design.\n \n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n In Radical Innovations of Software and Systems Engineering in the Future, 9th International Workshop, RISSEF 2002, Venice, Italy, October 7-11, 2002, Revised Papers, pages 198-203, 2002. \n \n\n\n\n
\n\n\n\n \n \n \"Module paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/rissef/Jackson02,\n  author    = {Daniel Jackson},\n  title     = {Module Dependences in Software Design},\n  booktitle = {Radical Innovations of Software and Systems Engineering\n               in the Future, 9th International Workshop, RISSEF 2002,\n               Venice, Italy, October 7-11, 2002, Revised Papers},\n  year      = {2002},\n  pages     = {198-203},\nurl_paper={pubs/2002/monterey.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2001\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A micromodularity mechanism.\n \n \n \n \n\n\n \n Jackson, D.; Shlyakhter, I.; and Sridharan, M.\n\n\n \n\n\n\n In ESEC / SIGSOFT FSE, pages 62-73, 2001. \n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/JacksonSS01,\n  author    = {Daniel Jackson and\n               Ilya Shlyakhter and\n               Manu Sridharan},\n  title     = {A micromodularity mechanism},\n  booktitle = {ESEC / SIGSOFT FSE},\n  year      = {2001},\n  pages     = {62-73},\nurl_paper={pubs/2001/micromodularity.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Lightweight Analysis of Object Interactions.\n \n \n \n \n\n\n \n Jackson, D.; and Fekete, A.\n\n\n \n\n\n\n In Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings, pages 492-513, 2001. \n \n\n\n\n
\n\n\n\n \n \n \"Lightweight paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/tacs/JacksonF01,\n  author    = {Daniel Jackson and\n               Alan Fekete},\n  title     = {Lightweight Analysis of Object Interactions},\n  booktitle = {Theoretical Aspects of Computer Software, 4th International\n               Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001,\n               Proceedings},\n  year      = {2001},\n  pages     = {492-513},\n url_paper={pubs/2001/tacs-01.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2000\n \n \n (9)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Redesigning Air Traffic Control: An Exercise in Software Design.\n \n \n \n \n\n\n \n Jackson, D.; and Chapin, J.\n\n\n \n\n\n\n IEEE Software, 17(3): 63-70. 2000.\n \n\n\n\n
\n\n\n\n \n \n \"Redesigning paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/software/JacksonC00,\n  author    = {Daniel Jackson and\n               John Chapin},\n  title     = {Redesigning Air Traffic Control: An Exercise in Software\n               Design},\n  journal   = {IEEE Software},\n  volume    = {17},\n  number    = {3},\n  year      = {2000},\n  pages     = {63-70},\nurl_paper={pubs/2000/ieee-software-ctas.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Software analysis: a roadmap.\n \n \n \n \n\n\n \n Jackson, D.; and Rinard, M. C.\n\n\n \n\n\n\n In 22nd International Conference on on Software Engineering, Future of Software Engineering Track, ICSE 2000, Limerick Ireland, June 4-11, 2000, pages 133-145, 2000. \n \n\n\n\n
\n\n\n\n \n \n \"Software paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/JacksonR00,\n  author    = {Daniel Jackson and\n               Martin C. Rinard},\n  title     = {Software analysis: a roadmap},\n  booktitle = {22nd International Conference on on Software Engineering,\n               Future of Software Engineering Track, ICSE 2000, Limerick\n               Ireland, June 4-11, 2000},\n  year      = {2000},\n  pages     = {133-145},\nurl_paper={pubs/2000/analysis-roadmap.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Alcoa: the alloy constraint analyzer.\n \n \n \n \n\n\n \n Jackson, D.; Schechter, I.; and Shlyakhter, I.\n\n\n \n\n\n\n In Proceedings of the 22nd International Conference on on Software Engineering, ICSE 2000, Limerick Ireland, June 4-11, 2000, pages 730-733, 2000. \n \n\n\n\n
\n\n\n\n \n \n \"Alcoa: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/JacksonSS00,\n  author    = {Daniel Jackson and\n               Ian Schechter and\n               Ilya Shlyakhter},\n  title     = {Alcoa: the alloy constraint analyzer},\n  booktitle = {Proceedings of the 22nd International Conference on on Software\n               Engineering, ICSE 2000, Limerick Ireland, June 4-11, 2000},\n  year      = {2000},\n  pages     = {730-733},\nurl_paper={pubs/TR/alcoa-overview.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Finding bugs with a constraint solver.\n \n \n \n \n\n\n \n Jackson, D.; and Vaziri, M.\n\n\n \n\n\n\n In ISSTA, pages 14-25, 2000. \n \n\n\n\n
\n\n\n\n \n \n \"Finding paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/issta/JacksonV00,\n  author    = {Daniel Jackson and\n               Mandana Vaziri},\n  title     = {Finding bugs with a constraint solver},\n  booktitle = {ISSTA},\n  year      = {2000},\n  pages     = {14-25},\n url_paper={pubs/2000/issta00.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer.\n \n \n \n \n\n\n \n Khurshid, S.; and Jackson, D.\n\n\n \n\n\n\n In ASE, pages 13-22, 2000. \n \n\n\n\n
\n\n\n\n \n \n \"Exploring paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/kbse/KhurshidJ00,\n  author    = {Sarfraz Khurshid and\n               Daniel Jackson},\n  title     = {Exploring the Design of an Intentional Naming Scheme with\n               an Automatic Constraint Analyzer},\n  booktitle = {ASE},\n  year      = {2000},\n  pages     = {13-22},\nurl_paper={pubs/2001/INS_TACAS01.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Enforcing Design Constraints with Object Logic.\n \n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n In Static Analysis, 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 1, 2000, Proceedings, pages 1-21, 2000. \n \n\n\n\n
\n\n\n\n \n \n \"Enforcing paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sas/Jackson00,\n  author    = {Daniel Jackson},\n  title     = {Enforcing Design Constraints with Object Logic},\n  booktitle = {Static Analysis, 7th International Symposium, SAS 2000,\n               Santa Barbara, CA, USA, June 29 - July 1, 2000, Proceedings},\n  year      = {2000},\n  pages     = {1-21},\n url_paper={pubs/2000/sas00.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automating first-order relational logic.\n \n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n In SIGSOFT FSE, pages 130-139, 2000. \n \n\n\n\n
\n\n\n\n \n \n \"Automating paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/Jackson00,\n  author    = {Daniel Jackson},\n  title     = {Automating first-order relational logic},\n  booktitle = {SIGSOFT FSE},\n  year      = {2000},\n  pages     = {130-139},\nurl_paper={pubs/2000/alcoa-algorithm.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n COM revisited: tool-assisted modelling of an architectural framework.\n \n \n \n \n\n\n \n Jackson, D.; and Sullivan, K. J.\n\n\n \n\n\n\n In SIGSOFT FSE, pages 149-158, 2000. \n \n\n\n\n
\n\n\n\n \n \n \"COM paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/JacksonS00,\n  author    = {Daniel Jackson and\n               Kevin J. Sullivan},\n  title     = {COM revisited: tool-assisted modelling of an architectural\n               framework},\n  booktitle = {SIGSOFT FSE},\n  year      = {2000},\n  pages     = {149-158},\n url_paper={pubs/2000/com-fse00.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Some Shortcomings of OCL, the Object Constraint Language of UML.\n \n \n \n \n\n\n \n Vaziri, M.; and Jackson, D.\n\n\n \n\n\n\n In TOOLS 2000: 34th International Conference on Technology of Object-Oriented Languages and Systems, 30 July - 3 August 2000, Santa Barbara, CA, USA, pages 555-562, 2000. \n \n\n\n\n
\n\n\n\n \n \n \"Some paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/tools/VaziriJ00,\n  author    = {Mandana Vaziri and\n               Daniel Jackson},\n  title     = {Some Shortcomings of OCL, the Object Constraint Language\n               of UML},\n  booktitle = {TOOLS 2000: 34th International Conference on Technology\n               of Object-Oriented Languages and Systems, 30 July - 3 August\n               2000, Santa Barbara, CA, USA},\n  year      = {2000},\n  pages     = {555-562},\n url_paper={pubs/1999/omg.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1999\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Nitpick Analysis of Mobile IPv6.\n \n \n \n \n\n\n \n Jackson, D.; Ng, Y.; and Wing, J. M.\n\n\n \n\n\n\n Formal Asp. Comput., 11(6): 591-615. 1999.\n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/fac/JacksonNW99,\n  author    = {Daniel Jackson and\n               Yu-Chung Ng and\n               Jeannette M. Wing},\n  title     = {A Nitpick Analysis of Mobile IPv6},\n  journal   = {Formal Asp. Comput.},\n  volume    = {11},\n  number    = {6},\n  year      = {1999},\n  pages     = {591-615},\nurl_paper={pubs/1999/mobileip.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Lightweight Extraction of Object Models from Bytecode.\n \n \n \n \n\n\n \n Jackson, D.; and Waingold, A.\n\n\n \n\n\n\n In Proceedings of the 1999 International Conference on Software Engineering, ICSE' 99, Los Angeles, CA, USA, May 16-22, 1999, pages 194-202, 1999. \n \n\n\n\n
\n\n\n\n \n \n \"Lightweight paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/JacksonW99,\n  author    = {Daniel Jackson and\n               Allison Waingold},\n  title     = {Lightweight Extraction of Object Models from Bytecode},\n  booktitle = {Proceedings of the 1999 International Conference on Software\n               Engineering, ICSE' 99, Los Angeles, CA, USA, May 16-22,\n               1999},\n  year      = {1999},\n  pages     = {194-202},\nurl_paper={pubs/2001/womble.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1998\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Isomorph-Free Model Enumeration: A New Method for Checking Relational Specifications.\n \n \n \n \n\n\n \n Jackson, D.; Jha, S.; and Damon, C.\n\n\n \n\n\n\n ACM Trans. Program. Lang. Syst., 20(2): 302-343. 1998.\n \n\n\n\n
\n\n\n\n \n \n \"Isomorph-Free paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/toplas/JacksonJD98,\n  author    = {Daniel Jackson and\n               Somesh Jha and\n               Craig Damon},\n  title     = {Isomorph-Free Model Enumeration: A New Method for Checking\n               Relational Specifications},\n  journal   = {ACM Trans. Program. Lang. Syst.},\n  volume    = {20},\n  number    = {2},\n  year      = {1998},\n  pages     = {302-343},\n url_paper={pubs/1999/toplas98.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An Intermedicate Design Language and Its Analysis.\n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n In SIGSOFT FSE, pages 121-130, 1998. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/Jackson98,\n  author    = {Daniel Jackson},\n  title     = {An Intermedicate Design Language and Its Analysis},\n  booktitle = {SIGSOFT FSE},\n  year      = {1998},\n  pages     = {121-130},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1997\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Lackwit: A Program Understanding Tool Based on Type Inference.\n \n \n \n \n\n\n \n O'Callahan, R.; and Jackson, D.\n\n\n \n\n\n\n In Pulling Together, Proceedings of the 19th International Conference on Software Engineering, Boston, Massachusetts, USA, May 17-23, 1997, pages 338-348, 1997. \n \n\n\n\n
\n\n\n\n \n \n \"Lackwit: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/OCallahanJ97,\n  author    = {Robert O'Callahan and\n               Daniel Jackson},\n  title     = {Lackwit: A Program Understanding Tool Based on Type Inference},\n  booktitle = {Pulling Together, Proceedings of the 19th International\n               Conference on Software Engineering, Boston, Massachusetts,\n               USA, May 17-23, 1997},\n  year      = {1997},\n  pages     = {338-348},\nurl_paper={pubs/1999/lackwit.pdf}\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1996\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n An Invitation to Formal Methods.\n \n \n \n\n\n \n Bowen, J. P.; Butler, R. W.; Dill, D. L.; Glass, R. L.; Gries, D.; Hall, A.; Hinchey, M. G.; Holloway, C. M.; Jackson, D.; Jones, C. B.; Lutz, M. J.; Parnas, D. L.; Rushby, J. M.; Wing, J. M.; and Zave, P.\n\n\n \n\n\n\n IEEE Computer, 29(4): 16-30. 1996.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/computer/BowenBDGGHHHJJLPRWZ96,\n  author    = {Jonathan P. Bowen and\n               Ricky W. Butler and\n               David L. Dill and\n               Robert L. Glass and\n               David Gries and\n               Anthony Hall and\n               Michael G. Hinchey and\n               C. Michael Holloway and\n               Daniel Jackson and\n               Cliff B. Jones and\n               Michael J. Lutz and\n               David Lorge Parnas and\n               John M. Rushby and\n               Jeannette M. Wing and\n               Pamela Zave},\n  title     = {An Invitation to Formal Methods},\n  journal   = {IEEE Computer},\n  volume    = {29},\n  number    = {4},\n  year      = {1996},\n  pages     = {16-30},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Do You Really Need Formal Requirements/Requirements Need Form, Maybe Formality (Point-Counterpoint).\n \n \n \n\n\n \n Lawrence, B.; and Jackson, D.\n\n\n \n\n\n\n IEEE Software, 13(2): 20. 1996.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/software/LawrenceJ96,\n  author    = {Brian Lawrence and\n               Daniel Jackson},\n  title     = {Do You Really Need Formal Requirements/Requirements Need\n               Form, Maybe Formality (Point-Counterpoint)},\n  journal   = {IEEE Software},\n  volume    = {13},\n  number    = {2},\n  year      = {1996},\n  pages     = {20},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector.\n \n \n \n\n\n \n Jackson, D.; and Damon, C.\n\n\n \n\n\n\n IEEE Trans. Software Eng., 22(7): 484-495. 1996.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/tse/JacksonD96,\n  author    = {Daniel Jackson and\n               Craig Damon},\n  title     = {Elements of Style: Analyzing a Software Design Feature with\n               a Counterexample Detector},\n  journal   = {IEEE Trans. Software Eng.},\n  volume    = {22},\n  number    = {7},\n  year      = {1996},\n  pages     = {484-495},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector.\n \n \n \n\n\n \n Jackson, D.; and Damon, C.\n\n\n \n\n\n\n In ISSTA, pages 239-249, 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/issta/JacksonD96,\n  author    = {Daniel Jackson and\n               Craig Damon},\n  title     = {Elements of Style: Analyzing a Software Design Feature with\n               a Counterexample Detector},\n  booktitle = {ISSTA},\n  year      = {1996},\n  pages     = {239-249},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Faster Checking of Software Specifications by Eliminating Isomorphs.\n \n \n \n\n\n \n Jackson, D.; Jha, S.; and Damon, C.\n\n\n \n\n\n\n In Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Florida, USA, January 21-24, 1996, pages 79-90, 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/popl/JacksonJD96,\n  author    = {Daniel Jackson and\n               Somesh Jha and\n               Craig Damon},\n  title     = {Faster Checking of Software Specifications by Eliminating\n               Isomorphs},\n  booktitle = {Conference Record of POPL'96: The 23rd ACM\n                  SIGPLAN-SIGACT Symposium on Principles of\n                  Programming Languages, Florida, USA, January 21-24,\n                  1996},\n  year      = {1996},\n  pages     = {79-90},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Checking Relational Specifications With Binary Decision Diagrams.\n \n \n \n\n\n \n Damon, C.; Jackson, D.; and Jha, S.\n\n\n \n\n\n\n In SIGSOFT FSE, pages 70-80, 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/DamonJJ96,\n  author    = {Craig Damon and\n               Daniel Jackson and\n               Somesh Jha},\n  title     = {Checking Relational Specifications With Binary Decision\n               Diagrams},\n  booktitle = {SIGSOFT FSE},\n  year      = {1996},\n  pages     = {70-80},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Efficient Search as a Means of Executing Specifications.\n \n \n \n\n\n \n Damon, C.; and Jackson, D.\n\n\n \n\n\n\n In Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS '96, Passau, Germany, March 27-29, 1996, Proceedings, pages 70-86, 1996. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/tacas/DamonJ96,\n  author    = {Craig Damon and\n               Daniel Jackson},\n  title     = {Efficient Search as a Means of Executing Specifications},\n  booktitle = {Tools and Algorithms for Construction and Analysis of Systems,\n               Second International Workshop, TACAS '96, Passau, Germany,\n               March 27-29, 1996, Proceedings},\n  year      = {1996},\n  pages     = {70-86},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1995\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Aspect: Detecting Bugs with Abstract Dependences.\n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n ACM Trans. Softw. Eng. Methodol., 4(2): 109-145. 1995.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/tosem/Jackson95,\n  author    = {Daniel Jackson},\n  title     = {Aspect: Detecting Bugs with Abstract Dependences},\n  journal   = {ACM Trans. Softw. Eng. Methodol.},\n  volume    = {4},\n  number    = {2},\n  year      = {1995},\n  pages     = {109-145},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Structuring Z Specifications with Views.\n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n ACM Trans. Softw. Eng. Methodol., 4(4): 365-389. 1995.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/tosem/Jackson95a,\n  author    = {Daniel Jackson},\n  title     = {Structuring Z Specifications with Views},\n  journal   = {ACM Trans. Softw. Eng. Methodol.},\n  volume    = {4},\n  number    = {4},\n  year      = {1995},\n  pages     = {365-389},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The CMU Master of Software Engineering Core Curriculum.\n \n \n \n\n\n \n Garlan, D.; Brown, A. W.; Jackson, D.; Tomayko, J. E.; and Wing, J. M.\n\n\n \n\n\n\n In Software Engineering Education, 8th SEI CSEE Conference, New Orleans, LA, USA, March 29 - April 1, 1995, Proceedings, pages 65-86, 1995. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/csee/GarlanBJTW95,\n  author    = {David Garlan and\n               Alan W. Brown and\n               Daniel Jackson and\n               James E. Tomayko and\n               Jeannette M. Wing},\n  title     = {The CMU Master of Software Engineering Core Curriculum},\n  booktitle = {Software Engineering Education, 8th SEI CSEE Conference,\n               New Orleans, LA, USA, March 29 - April 1, 1995, Proceedings},\n  year      = {1995},\n  pages     = {65-86},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1994\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Abstract Model Checking of Infinite Specifications.\n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n In FME '94: Industrial Benefit of Formal Methods, Second International Symposium of Formal Methods Europe, Barcelona, Spain, October 24-18, 1994, Proceedings, pages 519-531, 1994. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/fm/Jackson94,\n  author    = {Daniel Jackson},\n  title     = {Abstract Model Checking of Infinite Specifications},\n  booktitle = {FME '94: Industrial Benefit of Formal Methods, Second International\n               Symposium of Formal Methods Europe, Barcelona, Spain, October\n               24-18, 1994, Proceedings},\n  year      = {1994},\n  pages     = {519-531},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Semantic Diff: A Tool for Summarizing the Effects of Modifications.\n \n \n \n\n\n \n Jackson, D.; and Ladd, D. A.\n\n\n \n\n\n\n In Proceedings of the International Conference on Software Maintenance, ICSM 1994, Victoria, BC, Canada, September 1994, pages 243-252, 1994. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icsm/JacksonL94,\n  author    = {Daniel Jackson and\n               David A. Ladd},\n  title     = {Semantic Diff: A Tool for Summarizing the Effects of Modifications},\n  booktitle = {Proceedings of the International Conference on Software\n               Maintenance, ICSM 1994, Victoria, BC, Canada, September\n               1994},\n  year      = {1994},\n  pages     = {243-252},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A New Model of Program Dependences for Reverse Engineering.\n \n \n \n\n\n \n Jackson, D.; and Rollins, E. J.\n\n\n \n\n\n\n In SIGSOFT FSE, pages 2-10, 1994. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sigsoft/JacksonR94,\n  author    = {Daniel Jackson and\n               Eugene J. Rollins},\n  title     = {A New Model of Program Dependences for Reverse Engineering},\n  booktitle = {SIGSOFT FSE},\n  year      = {1994},\n  pages     = {2-10},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1993\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Abstract Analysis with Aspect.\n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n In ISSTA, pages 19-27, 1993. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/issta/Jackson93,\n  author    = {Daniel Jackson},\n  title     = {Abstract Analysis with Aspect},\n  booktitle = {ISSTA},\n  year      = {1993},\n  pages     = {19-27},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1991\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Aspect: An Economical Bug-Detector.\n \n \n \n\n\n \n Jackson, D.\n\n\n \n\n\n\n In Proceedings of the 13th International Conference on Software Engineering, Austin, TX, USA, May 13-17, 1991, pages 13-22, 1991. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/icse/Jackson91,\n  author    = {Daniel Jackson},\n  title     = {Aspect: An Economical Bug-Detector},\n  booktitle = {Proceedings of the 13th International Conference on Software\n               Engineering, Austin, TX, USA, May 13-17, 1991},\n  year      = {1991},\n  pages     = {13-22},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 1989\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Practical Specification Techniques for Control-Oriented Systems.\n \n \n \n\n\n \n Zave, P.; and Jackson, D.\n\n\n \n\n\n\n In IFIP Congress, pages 83-88, 1989. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/ifip/ZaveJ89,\n  author    = {Pamela Zave and\n               Daniel Jackson},\n  title     = {Practical Specification Techniques for Control-Oriented\n               Systems},\n  booktitle = {IFIP Congress},\n  year      = {1989},\n  pages     = {83-88},\n}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);