| [1] | IanJ. Hayes, LarissaA. Meinicke, and Naso Evangelou-Oost. Restructuring a concurrent refinement algebra, 2024. [bib| DOI| arXiv| http| Abstract] |
| [2] | IanJ. Hayes, LarissaA. Meinicke, and Naso Evangelou-Oost. Restructuring a concurrent refinement algebra. In Uli Fahrenberg, Wesley Fussner, and Roland Glück, editors, Relational and Algebraic Methods in Computer Science, volume 14787 of Lecture Notes in Computer Science, pages 135--155, Cham, 2024. Springer Nature Switzerland. [bib| Abstract] |
| [3] | LarissaA. Meinicke and IanJ. Hayes. Reasoning about distributive laws in a concurrent refinement algebra, 2024. [bib| DOI| arXiv| http] |
| [4] | LarissaA. Meinicke and IanJ. Hayes. Reasoning about distributive laws in a concurrent refinement algebra. In A.Cavalcanti and J.Baxter, editors, The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II, volume 14781 of Lecture Notes in Computer Science, pages 1--22, Cham, 2024. Springer Nature Switzerland. [bib| DOI| http| Abstract] |
| [5] | LarissaA. Meinicke, IanJ. Hayes, and CliffB. Jones. Data reification in a concurrent rely-guarantee algebra, 2024. [bib| DOI| arXiv| http] |
| [6] | IanJ. Hayes, CliffB. Jones, and LarissaA. Meinicke. Handling expression evaluation under interference, 2024. [bib| arXiv| http] |
| [7] | Naso Evangelou-Oost, Larissa Meinicke, Callum Bannister, and IanJ. Hayes. Trace models of concurrent valuation algebras, 2023. [bib| DOI| arXiv| http| Abstract] |
| [8] | LarissaA. Meinicke and IanJ. Hayes. Using cylindric algebra to support local variables in rely/guarantee concurrency. In 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), pages 108--119. IEEE, 2023. [bib| DOI| Abstract] |
| [9] | Mark Utting, BraeJ. Webb, and IanJ. Hayes. Differential testing of a verification framework for compiler optimizations (case study). In FormaliSE 2023. IEEE, 2023. [bib| Abstract] |
| [10] | Naso Evangelou-Oost, Larissa Meinicke, Callum Bannister, and IanJ. Hayes. Trace models of concurrent valuation algebras. In YiLi and Sofiène Tahar, editors, Formal Methods and Software Engineering (ICFEM 2023), volume 14308 of Lecture Notes in Computer Science, pages 118--136, Singapore, 2023. Springer Nature. [bib| DOI| Abstract] |
| [11] | IanJ. Hayes, Mark Utting, and BraeJ. Webb. Verifying compiler optimisations. In YiLi and Sofiène Tahar, editors, Formal Methods and Software Engineering (ICFEM 2023), volume 14308 of Lecture Notes in Computer Science, pages 3--8, Singapore, 2023. Springer Nature. Invited paper. [bib| DOI| Abstract] |
| [12] | BraeJ. Webb, IanJ. Hayes, and Mark Utting. Verifying term graph optimizations using Isabelle/HOL. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 320--333, New York, NY, USA, 2023. Association for Computing Machinery. [bib| DOI| http| Abstract] |
| [13] | IanJ. Hayes, CliffB. Jones, and LarissaA. Meinicke. Specifying and reasoning about shared-variable concurrency. In JonathanP. Bowen, Qin Li, and Qiwen Xu, editors, Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, volume 14080 of Lecture Notes in Computer Science, pages 110--135, Cham, 2023. Springer Nature Switzerland AG. [bib| DOI| Abstract] |
| [14] | Nasos Evangelou-Oost, Callum Bannister, and IanJ. Hayes. Contextuality in distributed systems. In Roland Glück, Luigi Santocanale, and Michael Winter, editors, Relational and Algebraic Methods in Computer Science (RAMiCS 2023), pages 52--68, Cham, 2023. Springer International Publishing. [bib| DOI| Abstract] |
| [15] | BraeJ. Webb, IanJ. Hayes, and Mark Utting. Verifying term graph optimizations using Isabelle/HOL, 2022. [bib| DOI| arXiv| http| Abstract] |
| [16] | Nasos Evangelou-Oost, Callum Bannister, and IanJ. Hayes. Contextuality in distributed systems, 2022. [bib| DOI| arXiv| http| Abstract] |
| [17] | BraeJ. Webb, Mark Utting, and IanJ. Hayes. A formal semantics of the GraalVM intermediate representation. In Zhe Hou and Vijay Ganesh, editors, Automated Technology for Verification and Analysis, volume 12971 of Lecture Notes in Computer Science, pages 111--126, Cham, October 2021. Springer International Publishing. [bib| DOI| Abstract] |
| [18] | B.Dongol, I.J. Hayes, and G.Struth. Convolution algebras: Relational convolution, generalised modalities and incidence algebras. Logical Methods in Computer Science, 17(1):13:1--13:34, February 2021. [bib| DOI| Abstract] |
| [19] | BraeJ. Webb, Mark Utting, and IanJ. Hayes. A formal semantics of the GraalVM intermediate representation, 2021. Ext. report at arXiv:2107.01815. [bib| arXiv| Abstract] |
| [20] | IanJ. Hayes, LarissaA. Meinicke, and PatrickA. Meiring. Deriving laws for developing concurrent programs in a rely-guarantee style, 2021. Ext. report at arXiv:2103.15292. [bib| arXiv| http] |
| [21] | IanJ. Hayes and Steve King. Software specification. In CliffB. Jones and Jayadev Misra, editors, Theories of Programming: The Life and Works of Tony Hoare, page 251–270, New York, NY, USA, 2021. Association for Computing Machinery. [bib| http] |
| [22] | A.Burns, I.J. Hayes, and C.B. Jones. Deriving specifications of control programs for cyber physical systems. The Computer Journal, 63(5):774--790, May 2020. [bib| DOI| http| Abstract] |
| [23] | I.J. Hayes and L.A. Meinicke. Developing an algebra for rely/guarantee concurrency: design decisions and challenges. In Pedro Ribeiro and Augusto Sampaio, editors, Unifying Theories of Programming 2019, volume 11885 of Lecture Notes in Computer Science, pages 176--197, Cham, October 2019. Springer International Publishing. [bib| DOI| Abstract] |
| [24] | IanJ. Hayes, LarissaA. Meinicke, Kirsten Winter, and RobertJ. Colvin. A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Formal Aspects of Computing, 31(2):133--163, April 2019. [bib| DOI| Abstract] |
| [25] | B.Dongol, I.J. Hayes, L.A. Meinicke, and G.Struth. Cylindric Kleene lattices for program construction. In G.Hutton, editor, Mathematics of Program Construction 2019, volume 11825 of Lecture Notes in Computer Science, pages 197--225, Cham, 2019. Springer International Publishing. [bib| DOI| Abstract] |
| [26] | LarissaA. Meinicke and IanJ. Hayes. Handling localisation in rely/guarantee concurrency: An algebraic approach, 2019. [bib| arXiv| http] |
| [27] | X.Wu, Y.Lu, P.Meiring, I.J. Hayes, and L.A. Meinicke. Type capabilities for object-oriented programming languages. In Jing Sun and Meng Sun, editors, Formal Methods and Software Engineering (ICFEM), volume 11232 of Lecture Notes in Computer Science, pages 215--230, Cham, November 2018. Springer International Publishing. [bib| DOI| Abstract] |
| [28] | I.J. Hayes. Engineering a theory of concurrent programming. In Jing Sun and Meng Sun, editors, Formal Methods and Software Engineering (ICFEM), volume 11232 of Lecture Notes in Computer Science, pages 3--18, Cham, November 2018. Springer International Publishing. Invited keynote paper. [bib| DOI| Abstract] |
| [29] | IanJ. Hayes. Some challenges of specifying concurrent program components. In John Derrick, Brijesh Dongol, and Steve Reeves, editors, Proceedings 18th Refinement Workshop, Oxford, UK, 18th July 2018, volume 282 of Electronic Proceedings in Theoretical Computer Science, pages 10--22. Open Publishing Association, October 2018. [bib| DOI| Abstract] |
| [30] | I.J. Hayes and L.A. Meinicke. Encoding fairness in a synchronous concurrent program algebra. In Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik deVink, editors, Formal Methods, Lecture Notes in Computer Science, pages 222--239, Cham, July 2018. Springer International Publishing. [bib| DOI| Abstract] |
| [31] | IanJ. Hayes and LarissaA. Meinicke. Encoding fairness in a synchronous concurrent program algebra: extended version with proofs, May 2018. [bib| arXiv| http] |
| [32] | I.J. Hayes and C.B. Jones. A guide to rely/guarantee thinking. In J.P. Bowen, Z.Liu, and Z.Zhang, editors, Engineering Trustworthy Software Systems, volume 11174 of Lecture Notes in Computer Science, pages 1--38, Cham, 2018. Springer International Publishing. [bib| DOI| Abstract] |
| [33] | Brijesh Dongol, Victor B.F. Gomes, IanJ. Hayes, and Georg Struth. Partial semigroups and convolution algebras. Archive of Formal Proofs, June 2017. https://www.isa-afp.org/entries/PSemigroupsConvolution.shtml, Formal proof development. [bib| Abstract] |
| [34] | R.J. Colvin, I.J. Hayes, and L.A. Meinicke. Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects of Computing, 29:853--875, 2017. Online 27 February 2017. [bib| Abstract] |
| [35] | IanJ. Hayes, XiWu, and LarissaA. Meinicke. Capabilities for Java: Secure access to resources. In Bor-YuhEvan Chang, editor, Programming Languages and Systems: 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings, pages 67--84, Cham, 2017. Springer International Publishing. [bib| DOI| http| Abstract] |
| [36] | IanJ. Hayes, LarissaA. Meinicke, Kirsten Winter, and RobertJ. Colvin. A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency, 2017. https://arxiv.org/abs/1710.03352. [bib| arXiv| http] |
| [37] | J.Fell, I.J. Hayes, and A.Velykis. Concurrent refinement algebra and rely quotients. Archive of Formal Proofs, December 2016. http://isa-afp.org/entries/Concurrent_Ref_Alg.shtml, Formal proof development. [bib| Abstract] |
| [38] | IanJ. Hayes. Generalised rely-guarantee concurrency: An algebraic foundation. Formal Aspects of Computing, 28(6):1057--1078, November 2016. [bib| DOI| http| Abstract] |
| [39] | I.J. Hayes, R.Colvin, L.Meinicke, K.Winter, and A.Velykis. An algebra of synchronous atomic steps, November 2016. http://dx.doi.org/10.1007/978-3-319-48989-6_22. [bib| arXiv| http| Abstract] |
| [40] | I.J. Hayes, R.Colvin, L.Meinicke, K.Winter, and A.Velykis. An algebra of synchronous atomic steps. In J.Fitzgerald, C.Heitmeyer, S.Gnesi, and A.Philippou, editors, FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 352--369, Cham, November 2016. Springer International Publishing. Best paper award. [bib| DOI| http| Abstract] |
| [41] | CliffB. Jones and IanJ. Hayes. Possible values: Exploring a concept for concurrency. Journal of Logical and Algebraic Methods in Programming, 85(5, Part 2):972--984, August 2016. [bib| DOI| http| Abstract] |
| [42] | B.Dongol, I.J. Hayes, and G.Struth. Convolution as a unifying concept: Applications in separation logic, interval calculi, and concurrency. ACM Trans. Comput. Logic, 17(3):15:1--15:25, February 2016. [bib| DOI| http| Abstract] |
| [43] | CliffB. Jones, IanJ. Hayes, and RobertJ. Colvin. Balancing expressiveness in formal approaches to concurrency. Formal Aspects of Computing, 27(3):475--497, May 2015. [bib| DOI| http| Abstract] |
| [44] | IanJ. Hayes. Separating concerns of rely and guarantee in concurrent program derivation. In DavidA. Naumann, editor, Unifying Theories of Programming, UTP 2014, volume 8963 of LNCS, pages vii--x. Springer, 2015. Invited keynote. [bib| Abstract] |
| [45] | IanJ. Hayes. Generalised rely-guarantee concurrency: An algebraic foundation, 2015. http://dx.doi.org/10.1007/s00165-012-??-1. [bib| arXiv| http| Abstract] |
| [46] | IanJ. Hayes, CliffB. Jones, and RobertJ. Colvin. Laws and semantics for rely-guarantee refinement. Technical Report CS-TR-1425, School of Computing Science, Newcastle University, July 2014. Superseded by [36] and other papers. 66 pages. [bib| Abstract] |
| [47] | Brijesh Dongol, IanJ. Hayes, and PeterJ. Robinson. Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects of Computing, 26(3):563--589, May 2014. [bib| DOI| http| Abstract] |
| [48] | Brijesh Dongol, IanJ. Hayes, and John Derrick. Deriving real-time action systems with multiple time bands using algebraic reasoning. Science of Computer Programming, 85 Part B:137--165, 2014. [bib| DOI| Abstract] |
| [49] | IanJ. Hayes. Towards structuring system specifications with time bands using layers of rely-guarantee conditions. In C.Artho and P.C. Ölveczky, editors, Formal Techniques for Safety-Critical Systems, volume 419 of Communications in Computer and Information Science, pages 1--2. Springer, 2014. [bib| DOI| Abstract] |
| [50] | IanJ. Hayes and Larissa Meinicke. Invariants, well-founded statements and real-time program algebra. In Cliff.B. Jones, P.Pihlajasaari, and Jun Sun, editors, Formal Methods (FM 2014), volume 8442 of LNCS, pages 318--334. Springer, 2014. [bib| Abstract] |
| [51] | IanJ. Hayes, CliffB. Jones, and RobertJ. Colvin. Reasoning about concurrent programs: Refining rely-guarantee thinking. Technical Report CS-TR-1395, School of Computing Science, Newcastle University, September 2013. Superseded by CS-TR-1425. 66 pages. [bib| Abstract] |
| [52] | I.J. Hayes, S.E. Dunne, and L.A. Meinicke. Linking unifying theories of program refinement. Science of Computer Programming, 78(11):2086--2107, 2013. [bib| DOI| http| Abstract] |
| [53] | Brijesh Dongol and IanJ. Hayes. Deriving real-time action systems in a sampling logic. Science of Computer Programming, 78(11):2047--2063, 2013. [bib| DOI| http| Abstract] |
| [54] | I.J. Hayes, A.Burns, B.Dongol, and C.B. Jones. Comparing degrees of non-deterministic in expression evaluation. The Computer Journal, 56(6):741--755, 2013. [bib| Abstract] |
| [55] | DanielR. Bradley and IanJ. Hayes. Visuocode: A software development environment that supports spatial navigation and composition. In Alexandru Telea, Andreas Kerren, and Andrian Marcus, editors, First IEEE Working Conference on Software Visualization (VISSOFT), pages 1--4. IEEE, 2013. [bib| DOI| http| Abstract] |
| [56] | Kirsten Winter, Chenyi Zhang, IanJ. Hayes, Nathan Keynes, Cristina Cifuentes, and Lian Li. Path-sensitive data flow analysis simplified. In Lindsay Groves and Jing Sun, editors, Formal Methods and Software Engineering: Proceedings 15th International Conference on Formal Engineering Methods (ICFEM), volume 8144 of LNCS, pages 415--430. Springer, 2013. [bib| DOI| http| Abstract] |
| [57] | B.Dongol and I.J. Hayes. Approximating idealised real-time specifications using time bands. In A.Romanovsky, C.B. Jones, J.Bendiposto, and M.Leuschel, editors, Automated Verification of Critical Systems 2011, volume46 of Electronic Communications of the EASST, pages 1--16. EASST, 2012. [bib| DOI| Abstract] |
| [58] | Eban Escott, Paul Strooper, Paul King, and Ian Hayes. Model-driven web form validation with UML and OCL. In Andreas Harth and Nora Koch, editors, Current Trends in Web Engineering, volume 7059 of Lecture Notes in Computer Science, pages 223--235. Springer Berlin / Heidelberg, 2012. [bib| http| Abstract] |
| [59] | Brijesh Dongol and IanJ. Hayes. Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. In John Derrick, Stefania Gnesi, Diego Latella, and Helen Treharne, editors, Integrated Formal Methods, volume 7321 of LNCS, pages 39--53. Springer, 2012. [bib| DOI| http| Abstract] |
| [60] | IanJ. Hayes and RobertJ. Colvin. Integrated operational semantics: Small-step, big-step and multi-step. In John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, and Elvinia Riccobene, editors, Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, volume 7316 of LNCS, pages 21--35. Springer, 2012. [bib| DOI| Abstract] |
| [61] | Brijesh Dongol and IanJ. Hayes. Deriving real-time action systems controllers from multiscale system specifications. In J.Gibbons and P.Nogueira, editors, Mathematics of Program Construction, volume 7342 of LNCS, pages 102--131. Springer, 2012. [bib| DOI| http| Abstract] |
| [62] | Brijesh Dongol, IanJ. Hayes, Larissa Meinicke, and Kim Solin. Towards an algebra for real-time programs. In W.Kahl and T.G. Griffin, editors, 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS), volume 7560 of LNCS, pages 50--65. Springer, 2012. [bib| DOI| http| Abstract] |
| [63] | Brijesh Dongol, John Derrick, and IanJ. Hayes. Fractional permissions and non-deterministic evaluators in interval temporal logic. In Gerald Lüttgen and Stephan Merz, editors, Proc. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), volume53 of Electronic Communications of the EASST, pages 1--15, 2012. [bib| DOI| Abstract] |
| [64] | I.J. Hayes, A.Burns, B.Dongol, and C.B. Jones. Comparing models of nondeterministic expression evaluation. Technical Report CS-TR-1273, School of Computing Science, Newcastle University, September 2011. [bib| Abstract] |
| [65] | R.J. Colvin and I.J. Hayes. A semantics for Behavior Trees using CSP with specification commands. Science of Computer Programming, 76(10):891--914, 2011. [bib| DOI| http| Abstract] |
| [66] | R.J. Colvin and I.J. Hayes. Structural operational semantics through context-dependent behaviour. Journal of Logic and Algebraic Programming, 80(7):392--426, 2011. [bib| DOI| Abstract] |
| [67] | Alan Burns, Kun Wei, Jim Woodcock, IanJ. Hayes, and CliffB. Jones. Timebands framework -- 2011. Technical Report YCS-2011-467, Department of Computer Science, University of York, 2011. 36 pages. [bib| Abstract] |
| [68] | Alan Burns and IanJ. Hayes. A timeband framework for modelling real-time systems. Real-Time Systems, 45(1--2):106--142, June 2010. [bib| DOI| http| Abstract] |
| [69] | SteveE. Dunne, IanJ. Hayes, and AndyJ. Galloway. Reasoning about loops in total and general correctness. In A.Butterfield, editor, Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, September 8-10, 2008, Revised Selected, volume 5713 of Lecture Notes in Computer Science, pages 62--81. Springer, 2010. [bib| DOI| Abstract] |
| [70] | Brijesh Dongol and IanJ. Hayes. Compositional action system derivation using enforced properties. In C.Bolduc, J.Desharnais, and B.Ktari, editors, Mathematics of Program Construction (MPC), volume 6120 of LNCS, pages 119--139. Springer Verlag, 2010. [bib| Abstract] |
| [71] | I.J. Hayes, S.E. Dunne, and L.A. Meinicke. Unifying theories of programming that distinguish nontermination and abort. In C.Bolduc, J.Desharnais, and B.Ktari, editors, Mathematics of Program Construction, volume 6120 of LNCS, pages 178--194. Springer, 2010. [bib| Abstract] |
| [72] | I.J. Hayes. Invariants and well-foundedness in program algebra. In A.Cavalcanti, D.Déharbe, M.-C. Gaudel, and J.Woodcock, editors, International Colloquium on Theoretical Aspects of Computing (ICTAC), volume 6255 of LNCS, pages 1--14. Springer, 2010. [bib| DOI| Abstract] |
| [73] | K.Winter, I.J. Hayes, and R.J. Colvin. Integrating requirements: The Behavior Tree philosophy. In J.L. Fiadeiro and S.Gnesi, editors, Proc. of Int. Conf. on Software Engineering and Formal Methods (SEFM 2010), pages 41--50. IEEE Computer Society Press, 2010. [bib| DOI| Abstract] |
| [74] | IanJ. Hayes. Dynamically detecting faults via integrity constraints. In Michael Butler, Cliff Jones, Alexander Romanovsky, and Elena Troubitsyna, editors, Methods, Models, and Tools for Fault Tolerance, volume 5454 of Lecture Notes in Computer Science, pages 85--103. Springer Verlag, 2009. [bib| Abstract] |
| [75] | R.J. Colvin and I.J. Hayes. CSP with hierarchical state. In M.Leuschel and H.Wehrheim, editors, Integrated Formal Methods (IFM 2009), volume 5423 of LNCS, pages 118--135. Springer, 2009. [bib| Abstract] |
| [76] | Brijesh Dongol and IanJ. Hayes. Enforcing safety and progress properties: An approach to concurrent program derivation. In Colin Fidge, editor, Australian Software Engineering Conference, pages 3--12. IEEE Computer Society, 2009. [bib| Abstract] |
| [77] | R.Colvin, I.J. Hayes, and P.A. Strooper. Calculating modules in contextual logic program refinement. Theory and Practice of Logic Programming, 8(01):1--31, 2008. [bib| DOI| arXiv| http| Abstract] |
| [78] | Larissa Meinicke and IanJ. Hayes. Algebraic reasoning for probabilistic action systems and while-loops. Acta Informatica, 45(5):321--382, 2008. [bib| DOI| Abstract] |
| [79] | Larissa Meinicke and IanJ. Hayes. Probabilistic choice in refinement algebra. In Philippe Audebaud and Christine Paulin-Mohring, editors, Mathematics of Program Construction (MPC), volume 5133 of Lecture Notes in Computer Science, pages 243--267. Springer Verlag, 2008. [bib| DOI| Abstract] |
| [80] | IanJ. Hayes. Towards reasoning about teleo-reactive programs for robust real-time systems. In Nicolas Guelfi, Henry Muccini, Patrizio Pelliccione, and Alexander Romanovsky, editors, Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems, pages 87--94, New York, NY, USA, 2008. ACM. [bib| DOI| Abstract] |
| [81] | R.Colvin and I.J. Hayes. A semantics for behavior trees. ACCS Technical Report ACCS-TR-07-01, ARC Centre for Complex Systems (ACCS), April 2007. [bib| http] |
| [82] | I.J. Hayes. Procedures and parameters in the real-time program refinement calculus. Science of Computer Programming, 64(3):286--311, February 2007. [bib| DOI| Abstract] |
| [83] | C.B. Jones, I.J. Hayes, and M.A. Jackson. Deriving specifications for systems that are connected to the physical world. In C.B. Jones, Z.Liu, and J.Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of Lecture Notes in Computer Science, pages 364--390. Springer Verlag, 2007. [bib| DOI| Abstract] |
| [84] | Brijesh Dongol and IanJ. Hayes. Trace semantics for the Owicki-Gries theory integrated with the progress logic from unity. Technical Report SSE-2007-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2007. [bib] |
| [85] | I.J. Hayes. Termination of real-time programs: definitely, definitely not or maybe. In S.E. Dunne and W.J. Stoddart, editors, UTP 2006: First Int. Symp. on Unifying Theories of Programming, volume 4010 of LNCS, pages 141--154. Springer, 2006. [bib| Abstract] |
| [86] | Larissa Meinicke and IanJ. Hayes. Continuous action system refinement. In T.Uustalu, editor, Mathematics of Program Construction: Proceedings 8th International Conference (MPC 2006), volume 4014 of LNCS, pages 316--337. Springer Verlag, 2006. [bib| DOI| http| Abstract] |
| [87] | L.Meinicke and I.J. Hayes. Reasoning algebraically about probabilistic loops. In Zhiming Liu and Jifeng He, editors, ICFEM, volume 4260 of LNCS, pages 380--399. Springer Verlag, 2006. [bib| DOI| http| Abstract] |
| [88] | I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. FACS FACTS, 2006-2:56--78, 2006. [bib] |
| [89] | K.Lermer, C.J. Fidge, and I.J. Hayes. A theory for execution-time derivation in real-time programs. Theoretical Computer Science, 346(1):3--27, November 2005. [bib| Abstract] |
| [90] | J.Fitzgerald, I.J. Hayes, and A.Tarlecki, editors. FM 2005: Formal Methods -- Proceedings 13th International Symposium of Formal Methods Europe, Newcastle, UK, July 2005, volume 3582 of Lecture Notes in Computer Science. Springer Verlag, July 2005. [bib] |
| [91] | Phil Cook, Jim Welsh, and IanJ. Hayes. Incremental semantic evaluation for interactive systems: Inertia, pre-emption, and relations. Technical Report SSE-2005-01, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2005. [bib] |
| [92] | Phil Cook, Jim Welsh, and IanJ. Hayes. Building a flexible incremental compiler back-end. Technical Report SSE-2005-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2005. [bib] |
| [93] | Erica Glynn, I.J. Hayes, and Anthony MacDonald. Integration of generic program analysis tools into a software development environment. In V.Estivill-Castro, editor, Computer Science 2005: Proceedings 28th Australasian Computer Science Conference (ACSC2005), volume38 of Conferences in Research and Practice in Information Technology, pages 249--257. Australian Computer Society, 2005. [bib| Abstract] |
| [94] | A.Burns, I.J. Hayes, G.Baxter, and C.J. Fidge. Modelling temporal behaviour in complex socio-technical systems. Technical Report YCS390, University of York, 2005. [bib| .html| .pdf] |
| [95] | I.J. Hayes. Towards platform-independent real-time systems. In P.A. Strooper, editor, ASWEC, pages 192--200. IEEE Computer Society, 2004. [bib| Abstract] |
| [96] | R.Colvin, L.Groves, I.J. Hayes, D.Hemer, R.Nickson, and P.A. Strooper. Developing logic programs from specifications using stepwise refinement. In Maurice Bruynooghe and Kung-Kiu Lau, editors, Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, volume 3049 of Lecture Notes in Computer Science, pages 66--89. Springer Verlag, 2004. [bib| Abstract] |
| [97] | C.Smith, K.Winter, I.J. Hayes, R.G. Dromey, P.A. Lindsay, and D.A. Carrington. An environment for building a system out of its requirements. In Proc. 19th IEEE Int. Conf. on Automated Software Engineering, pages 398--399. IEEE, 2004. [bib] |
| [98] | K.Lermer, C.J. Fidge, and I.J. Hayes. Linear approximation of execution-time constraints. Formal Aspects of Computing, 15(4):319--348, December 2003. [bib| Abstract] |
| [99] | K.Lermer, C.J. Fidge, and I.J. Hayes. Formal semantics for program paths. In J.Harland, editor, Computing: The Australian Theory Symposium (CATS) 2003, volume78 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 1--24. Elsevier, February 2003. [bib| .html| Abstract] |
| [100] | I.J. Hayes. A predicative semantics for real-time refinement. In A.McIver and C.C. Morgan, editors, Programming Methodology, pages 109--133. Springer, 2003. [bib| Abstract] |
| [101] | Sibylle Peuker and Ian Hayes. Reasoning about deadlines in concurrent real-time programs. In Michel Charpentier and Beverly Sanders, editors, Workshop on Formal Methods for Parallel Programming (FMPP 2003) in Proc. 17th International Parallel and Distributed Processing Symposium, pages 1--8. IEEE CS Press, 2003. [bib| http| Abstract] |
| [102] | R.Colvin, I.J. Hayes, D.Hemer, and P.A. Strooper. Refinement of higher-order logic programs. In M.Leuschel, editor, Proceedings of the International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2002), volume 2664 of Lecture Notes in Computer Science, pages 126--143. Springer, 2003. [bib| Abstract] |
| [103] | I.J. Hayes, M.A. Jackson, and C.B. Jones. Determining the specification of a control system from that of its environment. In K.Araki, S.Gnesi, and D.Mandrioli, editors, FME 2003: Formal Methods, volume 2805 of LNCS, pages 154--169. Springer Verlag, 2003. [bib| .pdf| Abstract] |
| [104] | I.J. Hayes. Programs as paths: An approach to timing constraint analysis. In JinSong Dong and Jim Woodcock, editors, ICFEM, volume 2885 of LNCS, pages 1--15. Springer Verlag, 2003. [bib| Abstract] |
| [105] | IanJ. Hayes. Block-structured (attribute) grammars. Technical Report 02-47, Software Verification Research Centre, The University of Queensland, December 2002. [bib| Abstract] |
| [106] | I.J. Hayes, R.Colvin, D.Hemer, P.A. Strooper, and R.Nickson. A refinement calculus for logic programs. Theory and Practice of Logic Programming, 2(4--5):425--460, July 2002. [bib| Abstract] |
| [107] | G.Smith and I.J. Hayes. An introduction to Real-Time Object-Z. Formal Aspects of Computing, 13(2):128--141, May 2002. [bib| Abstract] |
| [108] | I.J. Hayes. Reasoning about real-time repetitions: Terminating and nonterminating. Science of Computer Programming, 43(2--3):161--192, 2002. [bib| http| .pdf| Abstract] |
| [109] | D.Hemer, R.Colvin, I.Hayes, and P.Strooper. Don't care non-determinism in logic program refinement. In J.Harland, editor, Proceedings of Computing: the Australasian Theory Symposium (CATS 2002), volume61 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 1--21. Elsevier Science, 2002. [bib| Abstract] |
| [110] | R.Colvin, I.J. Hayes, D.Hemer, and P.A. Strooper. Translating refined logic programs to Mercury. In M.Oudshoorn, editor, Proceedings 25th Australasian Computer Science Conference (ACSC 2002), volume4 of Conferences in Research and Practice in Information Technology, pages 33--40. Australian Computer Society, 2002. [bib] |
| [111] | I.J. Hayes. Reasoning about timeouts. In EerkeA. Boiten and Bernhard Möller, editors, Proc. Mathematics of Program Construction, volume 2386 of Lecture Notes in Computer Science, pages 94--116. Springer, 2002. [bib| DOI| Abstract] |
| [112] | I.J. Hayes. The real-time refinement calculus: A foundation for machine-independent real-time programming. In J.Esparza and C.Lakos, editors, Proceedings 23rd International Conference on the Application and Theory of Petri Nets, volume 2360 of Lecture Notes in Computer Science, pages 44--58. Springer, 2002. Invited keynote paper. [bib| Abstract] |
| [113] | S.Peuker and I.J. Hayes. Towards a refinement calculus for concurrent real-time programs. In C.George and Huaikou Miao, editors, Formal Methods and Software Engineering (ICFEM), volume 2495 of LNCS, pages 335--347. Springer-Verlag, 2002. [bib| Abstract] |
| [114] | Jamie Shield and IanJ. Hayes. Refining object-oriented invariants and dynamic constraints. In P.A. Strooper and P.Muenchaisri, editors, Asian-Pacific Software Engineering Conference (APSEC), pages 52--61. IEEE Computer Society, 2002. [bib| DOI| http| Abstract] |
| [115] | R.Colvin, I.J. Hayes, D.Hemer, and P.Strooper. Extended abstract: Refinement of higher-order logic programs. In M.Leuschel and F.Bueno, editors, Pre-Proceedings of the International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2002), pages 136--141. School of Computer Science, Technical University of Madrid, 2002. Extended abstract. [bib] |
| [116] | Phil Cook, Jim Welsh, and IanJ. Hayes. Incremental context-sensitive evaluation in context. Technical Report 02-11, Software Verification Research Centre, The University of Queensland, 2002. [bib] |
| [117] | I.J. Hayes, C.J. Fidge, and K.Lermer. Semantic characterisation of dead control-flow paths. IEE Proceedings---Software, 148(6):175--186, December 2001. Awarded the 2001/2002 Mather Premium by the Institution of Electrical Engineers. [bib| .pdf| Abstract] |
| [118] | J.Shield, I.J. Hayes, and D.A. Carrington. Using theory interpretation to mechanise the reals in a theorem prover. In C.J. Fidge, editor, Computing: The Australian Theory Symposium (CATS), volume42 of Electronic Notes in Theoretical Computer Science, pages 266--281. Elsevier Science, 2001. URL: www.elsevier.nl/locate/entcs. [bib] |
| [119] | I.J. Hayes and M.Utting. A sequential real-time refinement calculus. Acta Informatica, 37(6):385--448, 2001. [bib| .pdf| Abstract] |
| [120] | R.Colvin, I.J. Hayes, and P.Strooper. A technique for modular logic program refinement. In Kung-Kiu Lau, editor, Logic-based Program Synthesis and Transformation (LOPSTR 2000) Selected Papers, volume 2402 of Lecture Notes in Computer Science, pages 38--56. Springer, 2001. [bib| DOI| Abstract] |
| [121] | D.Hemer, I.Hayes, and P.Strooper. Refinement calculus for logic programming in Isabelle/HOL. In R.Boulton and P.Jackson, editors, Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science, pages 249--264. Springer, 2001. [bib| Abstract] |
| [122] | I.J. Hayes, R.Nickson, P.Strooper, and R.Colvin. A declarative semantics for logic program refinement. Technical Report 00-30, Software Verification Research Centre, The University of Queensland, Brisbane 4072, Australia, November 2000. [bib| Abstract] |
| [123] | R.Colvin, I.J. Hayes, and P.Strooper. Refining logic programs using types. In Jenny Edwards, editor, Australasian Computer Science Conference (ACSC2000), pages 43--50. IEEE Computer Society, 2000. [bib| DOI| Abstract] |
| [124] | I.J. Hayes. Reasoning about non-terminating loops using deadline commands. In R.Backhouse and J.N. Oliveira, editors, Proc. Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 60--79. Springer, 2000. This paper is superseded by [108]. [bib| Abstract] |
| [125] | R.Colvin, I.J. Hayes, and P.Strooper. Modular logic program refinement. In Kung-Kiu Lau, editor, Pre-Proceedings of the Tenth International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2000), number UMCS-00-6-1 in Technical Report, pages 1--10. Department of Computer Science, Manchester University, 2000. Extended abstract. [bib| Abstract] |
| [126] | I.J. Hayes. Real-time program refinement using auxiliary variables. In M.Joseph, editor, Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1926 of LNCS, pages 170--184. Springer, 2000. [bib| Abstract] |
| [127] | G.Smith and I.J. Hayes. Structuring real-time Object-Z specifications. In W.Grieskamp, T.Santen, and W.J. Stoddart, editors, IFM'00: Proceedings of the 2nd International Conference on Integrated Formal Methods, volume 1945 of Lecture Notes in Computer Science, pages 97--115. Springer, 2000. [bib] |
| [128] | I.J. Hayes. Reasoning about real-time programs using idle-invariant assertions. In J.S. Dong, J.He, and M.Purvis, editors, Proceedings 7th Asia-Pacific Software Engineering Conference (APSEC 2000), pages 16--23. IEEE Computer Society, 2000. [bib| Abstract] |
| [129] | C.J. Fidge, I.J. Hayes, and G.Watson. The deadline command. IEE Proceedings---Software, 146(2):104--111, April 1999. [bib| .ps] |
| [130] | I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. In J.P. Bowen and M.G. Hinchey, editors, High-Integrity System Specification and Design, pages 563--581. Springer, 1999. (Previously published in IEE/BCS Software Engineering Journal, Vol. 4, No. 6, 330--338, November, 1989). [bib] |
| [131] | G.Smith and I.J. Hayes. Towards real-time Object-Z. In Keijiro Araki, Andy Galloway, and Kenji Taguchi, editors, IFM'99: Proceedings of the 1st International Conference on Integrated Formal Methods, pages 49--65. Springer, 1999. [bib] |
| [132] | C.J. Fidge, I.J. Hayes, B.P. Mahony, and A.K. Wabenhorst. Real-time specification and reasoning using maximal intervals. In W.C.H. Cheng and A.S.M. Sajeev, editors, PART'99: Proceedings of the 6th Australasian Conference on Parallel and Real-Time Systems, pages 344--354. Springer, 1999. [bib] |
| [133] | S.Grundon, I.J. Hayes, and C.J. Fidge. Timing constraint analysis. In C.McDonald, editor, Computer Science '98: Proc. 21st Australasian Computer Sci. Conf. (ACSC'98), pages 575--586. Springer, 1998. [bib] |
| [134] | I.J. Hayes and M.Utting. Deadlines are termination. In D.Gries and W.-P. deRoever, editors, IFIP TC2/WG2.2, 2.3 International Conference on Programming Concepts and Methods (PROCOMET'98), pages 186--204. Chapman and Hall, 1998. [bib| .pdf] |
| [135] | C.J. Fidge, I.J. Hayes, A.P. Martin, and A.K. Wabenhorst. A set-theoretic model for real-time specification and reasoning. In J.Jeuring, editor, Mathematics of Program Construction (MPC'98), volume 1422 of Lecture Notes in Computer Science, pages 188--206. Springer, 1998. [bib] |
| [136] | I.J. Hayes. Expressive power of specification languages. Formal Aspects of Computing, 10(2):187--192, 1998. [bib] |
| [137] | D.Carrington, I.Hayes, R.Nickson, G.Watson, and J.Welsh. A program refinement tool. Formal Aspects of Computing, 10(2):97--124, 1998. [bib| .ps] |
| [138] | R.Colvin, I.J. Hayes, and P.Strooper. Data refining logic programs. In J.Grundy, M.Schwenke, and T.Vickers, editors, International Refinement Workshop and Formal Methods Pacific 1998, Discrete Mathematics and Theoretical Computer Science, pages 100--116. Springer, 1998. [bib| Abstract] |
| [139] | L.P. Wildman and I.J. Hayes. Supporting contexts in the sequential real-time refinement calculus. In J.Grundy, M.Schwenke, and T.Vickers, editors, International Refinement Workshop and Formal Methods Pacific 1998, pages 352--369. Springer, 1998. [bib] |
| [140] | I.J. Hayes. Separating timing and calculation in real-time refinement. In J.Grundy, M.Schwenke, and T.Vickers, editors, Int. Refinement Workshop and Formal Methods Pacific 1998, pages 1--16. Springer, 1998. [bib| .pdf| Abstract] |
| [141] | C.J. Fidge, I.J. Hayes, and B.P. Mahony. Defining differentiation and integration in Z. In J.Staples, M.G. Hinchey, and Shaoying Liu, editors, Proceedings Second International Conference on Formal Engineering Methods (ICFEM'98), pages 64--73. IEEE Computer Society, 1998. [bib] |
| [142] | I.Hayes, R.Nickson, and P.Strooper. Refining specifications to logic programs. In J.Gallagher, editor, Logic Program Synthesis and Transformation. Proc. of the 6th Int. Workshop, LOPSTR'96, Stockholm, Sweden, August 1996, volume 1207 of Lecture Notes in Computer Science, pages 1--19. Springer, 1997. [bib] |
| [143] | I.J. Hayes and M.Utting. Coercing real-time refinement: A transmitter. In D.J. Duke and A.S. Evans, editors, BCS-FACS Northern Formal Methods Workshop (NFMW'96), Electronic Workshops in Computing. Springer, 1997. [bib| .pdf] |
| [144] | R.Nickson and I.J. Hayes. Supporting contexts in program refinement. Science of Computer Programming, 29(3):279--302, 1997. [bib| Abstract] |
| [145] | P.G. Bancroft and I.J. Hayes. Type extension and refinement. In L.Groves and S.Reeves, editors, Formal Methods Pacific (FMP'97), pages 23--39. Springer, 1997. [bib| Abstract] |
| [146] | R.Colvin, I.J. Hayes, R.Nickson, and P.A. Strooper. A tool for logic program refinement. In D.J. Duke and A.S. Evans, editors, Second BCS-FACS Northern Formal Methods Workshop (NFMW'97), Electronic Workshops in Computing. Springer, 1997. [bib] |
| [147] | C.J. Fidge, M.Utting, I.J. Hayes, and P.Kearney. The Quartz refinement method for real-time multi-tasking systems. In Fifth Australasian Refinement Workshop (ARW'96), April 1996. [bib] |
| [148] | I.J. Hayes and P.A. Strooper. Refining specifications to logic programs. In I.J. Hayes, editor, Proc. 5th Australasian Refinement Workshop, pages 1--13. Software Verification Research Centre, The University of Queensland, April 1996. Unrefereed. [bib| .html] |
| [149] | I.J. Hayes, editor. Proc. 5th Australasian Refinement Workshop. Software Verification Research Centre, The University of Queensland, April 1996. Unrefereed. [bib| http] |
| [150] | D.A. Carrington, I.J. Hayes, R.Nickson, G.Watson, and J.Welsh. Structured presentation of refinements and proofs. In Kotagiri Ramamohanarao, editor, Proc. 19th Australasian Computer Science Conference (ACSC'96), volume 18(1) of Australian Computer Science Communications, pages 87--96, February 1996. [bib] |
| [151] | C.J. Fidge, M.Utting, P.Kearney, and I.J. Hayes. Integrating real-time scheduling theory and program refinement. In M.-C. Gaudel and J.Woodcock, editors, FME'96: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 327--346. Springer, 1996. [bib] |
| [152] | D.A. Carrington, I.J. Hayes, R.Nickson, G.Watson, and J.Welsh. A tool for developing correct programs by refinement. In He Jifeng, editor, Proc. BCS 7th Refinement Workshop, Bath, UK, Electronic Workshops in Computing, pages 1--17. Springer, 1996. [bib] |
| [153] | I.J. Hayes. Supporting module reuse in refinement. Science of Computer Programming, 27(2):175--184, 1996. [bib] |
| [154] | I.J. Hayes. Specification models. In Proc. 7th International Conference on Putting into Practice Methods and Tools for Information Systems Design, 10--12 October, 1995, Nantes, pages 1--10, October 1995. Invited keynote paper. [bib] |
| [155] | Ray Nickson and Ian Hayes. Program window inference. In Proc. of the 4th Australasian Refinement Workshop (ARW'95), pages 43--65. School of Computer Science and Engineering, University of New South Wales, April 1995. Unrefereed. Also available as Technical Report UQ-SVRC-95-29, Software Verification Research Centre, University of Queensland. [bib] |
| [156] | David Carrington, Ian Hayes, Ray Nickson, Geoffrey Watson, and Jim Welsh. Requirements for a program refinement engine. In Proc. of the 4th Australasian Refinement Workshop (ARW'95), pages 67--83. School of Computer Science and Engineering, University of New South Wales, April 1995. [bib] |
| [157] | L.P. Wildman and I.J. Hayes. Composing grammar transformations to construct a specification of a parser. In Ramamohanarao Kotagiri, editor, Proc. 18th Australasian Computer Science Conference (ACSC'95), Glenelg, South Australia, Australian Computer Science Communications, volume 17(1), pages 556--562, February 1995. [bib| .pdf| Abstract] |
| [158] | Report ofthe Computer Science Action LearningGroup. Improving the quality of tutorial classes in computer science. Technical Report UQ-CS-322, Department of Computer Science, University of Queensland, 1995. [bib] |
| [159] | I.J. Hayes and B.P. Mahony. Using units of measurement in formal specifications. Formal Aspects of Computing, 7(3):329--347, 1995. [bib| .pdf] |
| [160] | P.Bancroft and I.J. Hayes. A formal semantics for a language with type extension. In ZUM'95: The Z Formal Specification Notation, Proc. 9th International Conference of Z Users, Limerick, Ireland, September 7--9, 1995, volume 967 of Lecture Notes in Computer Science, pages 299--314. Springer, 1995. [bib] |
| [161] | I.J. Hayes and J.W. Sanders. Specification by interface separation. Formal Aspects of Computing, 7(4):430--439, 1995. [bib| .pdf] |
| [162] | P.Bakker, D.A. Carrington, A.Goodchild, I.J. Hayes, H.Purchase, and P.A. Strooper. The communicating technologist: An educational challenge. In D.Budny and B.Herrick, editors, Frontiers in Education 25th Annual Conference, pages 4a4.1--4a4.4, Atlanta, Georgia, 1995. IEEE Press. [bib] |
| [163] | I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. ACM Software Engineering News, 19(3):75--81, July 1994. Unrefereed. Previously published in FACS Europe [177]. [bib] |
| [164] | B.P. Mahony, C.Millerchip, and I.J. Hayes. A boiler control system: Overview of a case study in timed refinement. In Diana DelBel Belluz and HerbertC. Ratz, editors, Software Safety: Everybody's Business, Proceedings of the 1993 International Invitational Workshop on Design and Review of Software-Controlled Safety-Related Systems, Ottawa, pages 189--208. The Institute of Risk Research, 1994. [bib] |
| [165] | I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. Technical report UMCS-93-8-1, Department of Computer Science, University of Manchester, August 1993. [bib| .ps] |
| [166] | B.P. Mahony, C.Millerchip, and I.J. Hayes. A boiler control system: A case study in timed refinement. In Diana DelBel Belluz, editor, Technical proceedings International Symposium on Design and Review of Software-Controlled Safety-Related Systems, Ottawa, June 1993. 50 pages. [bib| .ps] |
| [167] | P.Bancroft and I.J. Hayes. Refining a module with opaque types. In Gopal Gupta, George Mohay, and Rodney Topor, editors, Proceedings, 16th Australian Computer Science Conference, Brisbane, Australian Computer Science Communications, volume 15(1), pages 615--624, February 1993. [bib] |
| [168] | I.J. Hayes and L.P. Wildman. Towards libraries for Z. In J.P. Bowen and J.E. Nicholls, editors, Z User Workshop: Proceedings of the Seventh Annual Z User Meeting, London, December 1992, Workshops in Computing, pages 37--51. Springer, 1993. [bib| .pdf] |
| [169] | I.J. Hayes. CICS message system. In I.J. Hayes, editor, Specification Case Studies, pages 238--243. Prentice Hall International, second edition, 1993. [bib] |
| [170] | I.J. Hayes. CICS temporary storage. In I.J. Hayes, editor, Specification Case Studies, pages 226--237. Prentice Hall International, second edition, 1993. [bib] |
| [171] | I.J. Hayes. Applying formal specification to software development in industry. In I.J. Hayes, editor, Specification Case Studies, pages 181--201. Prentice Hall International, second edition, 1993. (Previously published in IEEE Transactions on Software Engineering [204]). [bib] |
| [172] | I.J. Hayes. Flexitime specification. In I.J. Hayes, editor, Specification Case Studies, pages 134--138. Prentice Hall International, second edition, 1993. [bib] |
| [173] | I.J. Hayes. Block-structured symbol table. In I.J. Hayes, editor, Specification Case Studies, pages 14--30. Prentice Hall International, second edition, 1993. [bib] |
| [174] | I.J. Hayes. Examples of specification using mathematics. In I.J. Hayes, editor, Specification Case Studies, pages 2--13. Prentice Hall International, second edition, 1993. [bib] |
| [175] | I.J. Hayes, editor. Specification Case Studies. Prentice Hall, second edition, 1993. [bib| .pdf] |
| [176] | D.A. Carrington, D.Duke, I.J. Hayes, and J.Welsh. Deriving modular designs from formal specifications. In Int. Symp. on the Foundations of Software Engineering (SIGSOFT'93), pages 89--98. ACM, 1993. [bib| .pdf] |
| [177] | I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. FACS Europe, 1(1):7--30, 1993. Unrefereed. Also published in ACM Software Engineering News, 19(3):75--81, July 1994. [bib] |
| [178] | I.J. Hayes. Multi-relations in Z: A cross between multi-sets and binary relations. Acta Informatica, 29(1):33--62, February 1992. [bib| .pdf] |
| [179] | C.A.R. Hoare, I.J. Hayes, He Jifeng, C.Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sørensen, J.M. Spivey, and B.A. Sufrin. Laws of programming. In Manfred Broy, editor, Programming and Mathematical Method, volume88 of NATO ASI Series F: Computer and Systems Sciences, pages 95--122. Springer, 1992. [bib] |
| [180] | I.J. Hayes. VDM and Z: A comparative case study. Formal Aspects of Computing, 4(1):76--99, 1992. [bib| .pdf] |
| [181] | B.P. Mahony and I.J. Hayes. A case-study in timed refinement: A mine pump. IEEE Trans. on Software Engineering, 18(9):817--826, 1992. [bib| .pdf] |
| [182] | N.Ward and I.J. Hayes. Applications of angelic nondeterminism. In P.A. Bailes, editor, Proc. 6th Australian Software Engineering Conference (ASWEC91), pages 391--404. Australian Computer Society, July 1991. [bib| .pdf] |
| [183] | I.J. Hayes. Interpretations of Z schema operators. In Z User Workshop: Proceedings of the Fifth Annual Z User Meeting, Oxford, December 1990, Workshops in Computing, pages 12--26. Springer, 1991. [bib] |
| [184] | B.P. Mahony and I.J. Hayes. A case study in timed refinement: A central heater. In Proc. BCS/FACS Fourth Refinement Workshop, Workshops in Computing, pages 138--149. Springer, January 1991. [bib| .pdf] |
| [185] | B.P. Mahony and I.J. Hayes. Using continuous real functions to model timed histories. In P.A. Bailes, editor, Proc. 6th Australian Software Engineering Conf. (ASWEC91), pages 257--270. Australian Comp. Soc., 1991. [bib| .pdf] |
| [186] | D.A. Carrington, I.J. Hayes, and J.Welsh. A syntax-directed editor for object-oriented specifications. In Proc. of Pacific TOOLS '90, pages 46--57, November 1990. [bib] |
| [187] | I.J. Hayes. Specifying physical limitations: A case study of an oscilloscope. Technical report 167, Department of Computer Science, University of Queensland, July 1990. [bib| .ps] |
| [188] | I.J. Hayes, M.Mowbray, and G.A. Rose. Signalling System No. 7: The network layer. In E.Brinksma, G.Scollo, and C.A. Vissers, editors, Protocol Specification, Testing and Verification, IX, pages 3--14. Elsevier Science Publishers B. V. (North-Holland), 1990. [bib] |
| [189] | I.J. Hayes. A generalisation of bags in Z. In J.E. Nicholls, editor, Z User Workshop: Proceedings of the Fourth Annual Z User Meeting, Oxford, December 1989, Workshops in Computing, pages 113--127. Springer, 1990. [bib] |
| [190] | I.J. Hayes. Applying formal specification to software development in industry. In RichardH. Thayer and Merlin Dorfman, editors, System and Software Requirements Engineering, pages 594--603. IEEE Computer Society Press Tutorial, 1990. (Previously published in IEEE Transactions on Software Engineering [204]). [bib] |
| [191] | I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. IEE/BCS Software Engineering Journal, 4(6):330--338, November 1989. [bib| DOI] |
| [192] | I.J. Hayes, R.Neucom, and J.Welsh. An editor for Z specifications. In Advance papers CASE'89, pages 1--13, 1989. [bib] |
| [193] | R.Duke, I.J. Hayes, and G.A. Rose. Verification of a cyclic retransmission protocol. Technical Report UQ-CS-92, Department of Computer Science, The University of Queensland, July 1988. [bib] |
| [194] | R.Duke, I.J. Hayes, P.King, and G.A. Rose. Protocol specification and verification using Z. In IFIP Eighth International Workshop on Protocol Specification, Testing and Verification, pages 33--46. North-Holland, 1988. [bib] |
| [195] | I.J. Hayes, R.Neucom, and J.Welsh. An editor for Z specifications. Technical report, Department of Computer Science, University of Queensland, 1988. [bib] |
| [196] | C.A.R. Hoare, I.J. Hayes, He Jifeng, C.Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sørensen, J.M. Spivey, and B.A. Sufrin. Laws of programming. Communications of the ACM, 30(8):672--686, August 1987. Corrigenda: CACM 30(9):770. [bib] |
| [197] | G.A. Rose, R.Duke, and I.J. Hayes. Specifying communications services and protocols. In Proc 2nd Australian Software Engineering Conference (ASWEC-87), pages 161--170, Canberra, May 1987. IREE (Australia). [bib] |
| [198] | I.J. Hayes. Correctness of data representations. In Proc. 2nd Australian Software Engineering Conference (ASWEC-87), pages 75--86, Canberra, May 1987. IREE (Australia). [bib] |
| [199] | I.J. Hayes and K.A. Robinson. A Modula-2-based translator generator. Technical report 84, Department of Computer Science, University of Queensland, Brisbane, Australia, 1987. [bib] |
| [200] | I.J. Hayes, editor. Specification Case Studies. Prentice Hall International, 1987. [bib] |
| [201] | I.J. Hayes. Using mathematics to specify software. In Proc. 1st Australian Software Engineering Conference (ASWEC-86), pages 67--71, Canberra, May 1986. Institution of Engineers, Australia. At the 10th ASWEC Conference in 1997 this paper was given the award of Most Influential Paper of ASWEC'86, the first ASWEC Conference. [bib| .pdf] |
| [202] | I.J. Hayes. Specification directed module testing. IEEE Transactions on Software Engineering, SE-12(1):124--133, January 1986. [bib| .pdf] |
| [203] | I.J. Hayes. Weakest pre-specifications: weakest pre-conditions for procedures. In Proc. 9th Australian Computer Science Conference, pages 299--308, Canberra, January 1986. [bib] |
| [204] | I.J. Hayes. Applying formal specification to software development in industry. IEEE Transactions on Software Engineering, SE-11(2):169--178, February 1985. [bib| .pdf] |
| [205] | I.J. Hayes. Computer Architecture: The hardware/software interface. Ph. D. thesis, Department of Computer Science, University of New South Wales, Sydney, Australia, 1983. [bib] |
| [206] | I.J. Hayes and K.A. Robinson. A tutorial on Llama: A Pascal-based translator generator. Technical report, Department of Computer Science, University of New South Wales, Sydney, Australia, 1982. [bib] |
This file was generated by bibtex2html 1.99.
Last updated: Wed 16 Oct 2024 10:29:58 AEST
