\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 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 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 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 \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 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 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 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 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 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 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 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 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 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{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 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 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 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 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 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 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 \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 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 2016\n \n \n (8)\n \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 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 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 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 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 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 \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 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 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{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 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 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 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 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 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 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 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 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 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 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 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 \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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 \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 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 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 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 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 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 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 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 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 \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 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 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 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 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 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 \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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 \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 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 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
\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 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 1996\n \n \n (7)\n \n \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 \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