Bibliography¶
Daniel Jackson: Software Abstractions: Logic, Language, and Analysis. Revised edition. MIT Press, 2012.
Nuno Macedo, Alcino Cunha, José Pereira, Renato Carvalho, Ricardo Silva, Ana C. R. Paiva, Miguel Sozinho Ramalho, Daniel Castro Silva: Experiences on Teaching Alloy with an Automated Assessment Platform. Science of Computer Programming 211: 102690. Springer, 2021.
Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, Denis Kuperberg: Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. In proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE): 373-383. ACM, 2016.
Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo: The Electrum Analyzer: Model Checking Relational First-order Temporal Specifications. In proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE): 884-887. ACM, 2018.
Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo: Simulation under Arbitrary Temporal Logic Constraints. In proceedings of the 5th International Workshop on Formal Integrated Development Environment (F-IDE), EPTCS 310: 63-69. OPA, 2019.
Daniel Jackson: Alloy: A Language and Tool for Exploring Software Designs. Communications of the ACM 62(9): 66-76. ACM, 2019.
Daniel Jackson: The Essence of Software: Why Concepts Matter for Great Design. Princeton University Press, 2021.
Leslie Lamport: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16(3): 872-923. ACM, 1994.
Jonathan Edwards, Daniel Jackson, Emina Torlak: A Type System for Object Models. In proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE): 189-199. ACM, 2004.
Derek Rayside, Felix Sheng-Ho Chang, Greg Dennis, Robert Seater, Daniel Jackson: Automatic Visualization of Relational Logic Models. In proceedings of the Workshop on the Layout of (Software) Engineering Diagrams (LED), ECEASST 7. EASST, 2007.
Ernest J. H. Chang, Rosemary Roberts: An Improved Algorithm for Decentralized Extrema-Finding in Circular Configurations of Processes. Communications of the ACM 22(5): 281-283. ACM, 1979.
Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout: Reasoning with Temporal Logic on Truncated Paths. In proceedings of the 15th International Conference on Computer Aided Verification (CAV), LNCS 2725: 27-39. Springer, 2003.
Amir Pnueli: The Temporal Logic of Programs. In proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS): 46-57. IEEE, 1977.
Dov Gabbay, Amir Pnueli, Saharon Shelah, Jonathan Stavi: On the Temporal Analysis of Fairness. In proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL): 163-173. ACM, 1980.
Nicolas Markey: Temporal Logic with Past is Exponentially More Succinct. Bulletin of the European Association for Theoretical Computer Science 79: 122-128. EATCS, 2003.
Edmund M. Clarke, E. Allen Emerson: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In proceedings of the Workshop of Logics of Programs, LNCS 131: 52-71. Springer, 1981.
Rajeev Alur, David Dill, Costas Courcoubetis: Model-Checking for Real-Time Systems. In proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS). IEEE, 1990.
Aravinda Prasad Sistla, Edmund M. Clarke: The Complexity of Propositional Linear Temporal Logics. Journal of the ACM 32(3): 733-749. ACM, 1985.
Leslie Lamport: Proving the Correctness of Multiprocess Programs. Transaction of Software Engineering SE 3(2): 125-143. IEEE, 1977.
Bowen Halpern, Fred B. Schneider: Defining Liveness. Information Processsing Letters 21(4): 181-185. Elsevier, 1985.
Aravinda Prasad Sistla: Safety, Liveness, and Fairness in Temporal Logic. Formal Aspects of Computing 6(5): 495-512. ACM. 1994
Grgur Petric Maretic, Mohammad Torabi Dashti, David Basin: LTL is Closed under Topological Closure. Information Processsing Letters 114(8): 408-413. Elsevier, 2014.
Martın Abadi, Leslie Lamport: The Existence of Refinement Mappings. Theoretical Computer Science 82(2): 253–284. Elsevier, 1991
Aleksandar Milicevic, Joseph P. Near, Eunsuk Kang, Daniel Jackson: Alloy*: A General-purpose Higher-order Relational Constraint Solver. Formal Methods in System Design 55(1): 1-32. Springer, 2019.
Changjian Zhang, Ryan Wagner, Pedro Orvalho, David Garlan, Vasco M. Manquinho, Ruben Martins, Eunsuk Kang: AlloyMax: Bringing Maximum Satisfaction to Relational Specifications. In proceedings of the 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE): 155-167. ACM, 2021.
Germán Regis, César Cornejo, Simón Gutiérrez Brida, Mariano Politano, Fernando D. Raverta, Pablo Ponzio, Nazareno Aguirre, Juan Pablo Galeotti, Marcelo F. Frias: DynAlloy Analyzer: A Tool for the Specification and Analysis of Alloy Models with Dynamic Behaviour. In proceedings of the 11th Joint Meeting on Foundations of Software Engineering (ESEC/FSE): 969-973. ACM, 2017.
Pedro Silva, José N. Oliveira, Nuno Macedo, Alcino Cunha: Quantitative Relational Modelling with QAlloy. In proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE): 885-896. ACM, 2022.