|
2001 Conference Publication Using theory interpretation to mechanise the reals in a theorem proverShield, J., Hayes, I. J. and Carrington, D. A. (2001). Using theory interpretation to mechanise the reals in a theorem prover. CATS2001, Gold Coast, 29 January-1 February, 2001. Oxford: Elsevier. |
|
2001 Journal Article A sequential real-time refinement calculusHayes, I. J. and Utting, M. (2001). A sequential real-time refinement calculus. Acta Informatica, 37 (6), 385-448. doi: 10.1007/PL00013311 |
|
2001 Conference Publication Refinement Calculus for Logic Programming in Isabelle/HOLHemer, David, Hayes, Ian and Strooper, Paul (2001). Refinement Calculus for Logic Programming in Isabelle/HOL. TPHOLs: International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, UK, 3–6 September 2001 . Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-44755-5_18 |
|
2001 Conference Publication A technique for modular logic program refinementColvin, Robert, Hayes, Ian and Strooper, Paul (2001). A technique for modular logic program refinement. Tenth International Workshop on Logic-Based Program Synthesis and Transformation, London, England, 24-28 July, 2001. Berlin: Springer-Verlag. doi: 10.1007/3-540-45142-0_3 |
|
2000 Conference Publication Real-time program refinement using auxiliary variablesHayes, I. J. (2000). Real-time program refinement using auxiliary variables. Formal Techniques in Real-Time and Fault-Tolerant Systems, 6th International Symposium, Pune, India, 20-22 September 2000. Berlin, Germany: Springer. doi: 10.1007/3-540-45352-0_15 |
|
2000 Conference Publication Refining logic programs using typesColvin, Robert, Hayes, Ian J. and Strooper, Paul A. (2000). Refining logic programs using types. ACSC 2000, Canberra, ACT, Australia, 31 January - 3 February, 2000. Los Alamitos, CA, USA: IEEE Computer Society. doi: 10.1109/ACSC.2000.824379 |
|
2000 Conference Publication Reasoning about real-time programs using idle-invariant assertionsHayes, I. J. (2000). Reasoning about real-time programs using idle-invariant assertions. APSEC 2000, Singapore, 5-8 December 2000. Washington: IEEE Computer Society. doi: 10.1109/APSEC.2000.896678 |
|
2000 Conference Publication Structuring real-time Object-Z specificationsSmith, G and Hayes, I (2000). Structuring real-time Object-Z specifications. Integrated Formal Methods: Second International Conference, IFM 2000,, Dagstuhl Castle, Germany, November 2000. Berlin, Germany: Springer. doi: 10.1007/3-540-40911-4_7 |
|
2000 Conference Publication Reasoning about non-terminating loops using deadline commandsHayes, I. J. (2000). Reasoning about non-terminating loops using deadline commands. MPC 2000, Ponte de Lima, Portugal, 3-5 July 2000. Berlin: Springer. doi: 10.1007/10722010_5 |
|
1999 Book Refining logic programs using types and invariantsColvin, Rob, Hayes, Ian and Strooper, Paul (1999). Refining logic programs using types and invariants. SVRC Technical Report, 99-25. Software Verification Research Centre, School of Information Technology and Electrical Engineering, The University of Queensland. |
|
1999 Book Semantic identification of dead control-flow pathsHayes, Ian, Fidge, Colin and Lermer, Karl (1999). Semantic identification of dead control-flow paths. SVRC Technical Report, 99-32. Software Verification Research Centre, School of Information Technology and Electrical Engineering, The University of Queensland. |
|
1999 Book Real-time specification and reasoning using maximal intervalsFidge, C. J., Hayes, I. J., Mahony, B. P. and Wabenhorst, A. K. (1999). Real-time specification and reasoning using maximal intervals. SVRC Technical Report, 99-29. Software Verification Research Centre, School of Information Technology, The University of Queensland. |
|
1999 Book Towards real-time object-ZSmith, Graeme and Hayes, Ian (1999). Towards real-time object-Z. Technical Report SSE, 99-10. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland. |
|
1999 Journal Article The deadline commandFidge, C. J., Hayes, I. J. and Watson, G. N. (1999). The deadline command. IEE Proceedings - Software, 146 (2), 104-111. doi: 10.1049/ip-sen:19990407 |
|
1999 Book Chapter Specifications are not (necessarily) executableHayes, I. J. and Jones, C. B. (1999). Specifications are not (necessarily) executable. High-integrity system specification and design. (pp. 563-581) edited by J. P. Bowen and M. G. Hinchey. London: Springer. |
|
1999 Conference Publication Towards real-time Object-ZSmith, G. P. and Hayes, I. J. (1999). Towards real-time Object-Z. Integrated Formal Methods IFM'99, York, UK, 28-29 June 1999. London: Springer-Verlag. doi: 10.1007/978-1-4471-0851-1_4 |
|
1999 Conference Publication Real-time specification and reasoning using maximal intervalsFidge, C. J., Hayes, I. J., Mahony, B. and Wabenhorst, A. K. (1999). Real-time specification and reasoning using maximal intervals. PART '99, Melbourne, Australia, 29 Nov - 1 Dec 1999. Singapore: Springer-Verlag. |
|
1998 Book Defining Differentiation and Integration in ZFidge, Colin. J., Hayes, Ian. J. and Mahony, B. P. (1998). Defining Differentiation and Integration in Z. SVRC Technical Report, 98-09. Software Verification Research Centre, School of Information Technology, The University of Queensland. |
|
1998 Journal Article Expressive Power of Specification LanguagesHayes, Ian J. (1998). Expressive Power of Specification Languages. Formal Aspects of Computing, 10 (2), 187-192. doi: 10.1007/s001650050010 |
|
1998 Conference Publication A set-theoretic model for real-time specification and reasoningFidge, C. J., Hayes, I. J., Martin, A. P. and Wabenhorst, A. K. (1998). A set-theoretic model for real-time specification and reasoning. 4th International Conference on Mathematics of Program Construction, MPC 1998, Marstrand, June 15- 17 1998. Germany: Springer Verlag. doi: 10.1007/bfb0054291 |
