Dr Robert Colvin
Honorary Senior Fellow & Honorary Senior Fellow
School of Electrical Engineering and Computer Science
+61 7 336 51629
| Featured projects | Duration |
|---|---|
| Program Analysis Cell | 2018 |
Publications
Book Chapters
Colvin, Robert J., Hayes, Ian J., Heiner, Scott, Höfner, Peter, Meinicke, Larissa and Su, Roger C. (2024). Practical rely/guarantee verification of an efficient lock for seL4 on multicore architectures. The practice of formal methods: essays in honour of Cliff Jones, Part I. (pp. 65-87) edited by Ana Cavalcanti and James Baxter. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-66676-6_4
Colvin, Robert J. (2023). A fine-grained semantics for arrays and pointers under weak memory models. Formal methods : 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings. (pp. 301-320) edited by Marsha Chechik, Joost-Pieter Katoen and Martin Leucker. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-031-27481-7_18
Colvin, Robert, Groves, Lindsay, Hayes, Ian J., Hemer, David, Nickson, Ray and Strooper, Paul (2004). Developing logic programs from specifications using stepwise refinement. Program Development in Computational Logic. (pp. 66-89) edited by Maurice Bruynooghe and Kunk-Kiu Lau. Berlin: Springer Verlag. doi: 10.1007/978-3-540-25951-0_3
Journal Articles
Smith, Graeme, Winter, Kirsten and Colvin, Robert J. (2019). Linearizability on hardware weak memory models. Formal Aspects of Computing, 32 (1), 1-32. doi: 10.1007/s00165-019-00499-8
Hayes, Ian J., Meinicke, Larissa A., Winter, Kirsten and Colvin, Robert J. (2018). A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Formal Aspects of Computing, 31 (2), 133-163. doi: 10.1007/s00165-018-0464-4
Colvin, Robert J., Hayes, Ian J. and Meinicke, Larissa A. (2017). Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects of Computing, 29 (5), 1-23. doi: 10.1007/s00165-017-0416-4
Colvin, Robert J. (2016). Modeling and analysing neural networks using a hybrid process algebra. Theoretical Computer Science, 623, 15-64. doi: 10.1016/j.tcs.2015.08.019
Jones, Cliff B., Hayes, Ian J. and Colvin, Robert J. (2014). Balancing expressiveness in formal approaches to concurrency. Formal Aspects of Computing, 27 (3), 1-23. doi: 10.1007/s00165-014-0310-2
Colvin, Robert (2013). An operational semantics for object-oriented concepts based on the class hierarchy. Formal Aspects of Computing, 26 (3), 491-535. doi: 10.1007/s00165-012-0259-y
Colvin, Robert J. and Hayes, Ian J. (2011). A semantics for Behavior Trees using CSP with specification commands. Science of Computer Programming, 76 (10), 891-914. doi: 10.1016/j.scico.2010.11.007
Colvin, Robert J. and Hayes, Ian J. (2011). Structural operational semantics through context-dependent behaviour. Journal of Logic and Algebraic Programming, 80 (7), 392-426. doi: 10.1016/j.jlap.2011.05.001
Groves, Lindsay and Colvin, Robert (2009). Trace-based derivation of a scalable lock-free stack algorithm. Formal Aspects of Computing, 21 (1-2), 187-223. doi: 10.1007/s00165-008-0092-5
Colvin, Robert and Dongol, Brijesh (2009). A general technique for proving lock-freedom. Science of Computer Programming, 74 (3), 143-165. doi: 10.1016/j.scico.2008.09.013
Colvin, Robert, Grunske, Lars and Winter, Kirsten (2008). Timed behavior trees for failure mode and effects analysis of time-critical systems. Journal of Systems and Software, 81 (12), 2163-2182. doi: 10.1016/j.jss.2008.04.035
Colvin, Robert, Hayes, Ian J. and Strooper, Paul A. (2008). Calculating modules in contextual logic program refinement. Theory and Practice of Logic Programming, 8 (1), 1-31. doi: 10.1017/S1471068407003043
Groves, Lindsay and Colvin, Robert (2007). Derivation of a Scalable Lock-Free Stack Algorithm. Electronic Notes in Theoretical Computer Science, 187, 55-74. doi: 10.1016/j.entcs.2006.08.044
Hayes, Ian, Colvin, Robert, Hemer, David, Strooper, Paul and Nickson, Ray (2002). A refinement calculus for logic programs. Theory And Practice of Logic Programming, 2 (Part 4-5), 425-460. doi: 10.1017/S1471068402001448
Conference Papers
Colvin, Robert J. (2022). Separation of concerning things: a simpler basis for defining and programming with the C/C++ memory model. 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, 24-27 October 2022. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-031-17244-1_5
Colvin, Robert J. (2021). Parallelized Sequential Composition and Hardware Weak Memory Models. 19th International Conference on Software Engineering and Formal Methods (SEFM), Online, 6-10 December 2021. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-92124-8_12
Colvin, Robert J. and Winter, Kirsten (2020). An abstract semantics of speculative execution for reasoning about security vulnerabilities. Formal Methods. FM 2019 International Workshops, Porto, Portugal, 7–11 October 2019. Heidelberg, Germany: Springer. doi: 10.1007/978-3-030-54997-8_21
Colvin, Robert J. and Smith, Graeme (2018). A wide-spectrum language for verification of programs on weak memory models. 22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 15-17 July 2018. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-95582-7_14
Smith, Graeme, Winter, Kirsten and Colvin, Robert J. (2018). Correctness of concurrent objects under weak memory models. 18th Refinement Workshop, Refine 2018, Oxford, United Kingdom, 18 July 2018. SYDNEY: Open Publishing Association. doi: 10.4204/EPTCS.282.5
Hayes, Ian J., Colvin, Robert J., Meinicke, Larissa A., Winter, Kirsten and Velykis, Andrius (2016). An algebra of synchronous atomic steps. 21st International Symposium on Formal Methods, FM 2016, Limassol, Cyprus, 9-11 November 2016. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-48989-6_22
Hayes, Ian J. and Colvin, Robert J. (2012). Integrated operational semantics: small-step, big-step and multi-step. 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012), Pisa, Italy, 18-21 June 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-30885-7_2
Winter, Kirsten, Hayes, Ian J. and Colvin, Robert (2010). Integrating requirements: The behavior tree philosophy. Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, 13-18 September 2010. United States: IEEE Computer Society. doi: 10.1109/SEFM.2010.13
Winter, Kirsten, Colvin, Robert and Dromey, R, Geoff (2009). Dynamic relational behaviour for large-scale systems. 20th Australian Software Engineering Conference, Gold Coast, Australia, 14-17 April, 2009. U.S.A.: IEEE Computer Society Press. doi: 10.1109/ASWEC.2009.41
Colvin, Robert and Hayes, Ian J. (2009). CSP with hierarchical state. 7th International Conference on Integrated Formal Methods: IFM 2009, Dusseldorf, Germany, 16-19 February 2009. New York , U.S.A: Springer-Verlag. doi: 10.1007/978-3-642-00255-7_9
Colvin, Robert, Grunske, Lars and Winter, Kirsten (2007). Probabilistic timed behavior trees. Integrated Formal Methods 2007, Oxford, UK, 2-5 July, 2007. New York, U.S.: Elsevier North-Holland. doi: 10.1007/978-3-540-73210-5_9
Colvin, Robert and Groves, Lindsay (2007). Derivation of a scalable lock-free stack algorithm. 11th Refinement Workshop (REFINE 2006), Macao, China, 31 October 2006. Amsterdam, Netherlands: Elsevier. doi: 10.1016/j.entcs.2006.08.044
Wen, Lian, Colvin, Robert, Lin, Kai, Seagrott, John, Yatapanage, Nisansala and Dromey, Geoff (2007). 'Integrare', a collaborative environment for behavior-oriented design. 4th International Conference, CDVE 2007 Cooperative Design, Visualization, and Engineering, Shanghai, China, 16-20 September 2007. Berlin, Germany: Springer. doi: 10.1007/978-3-540-74780-2_14
Grunske, L., Colvin, R. and Winter, K. (2007). Probabilistic model-checking support for FMEA. Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), Edinburgh, Scotland, 17-19 September, 2007. Los Alamitos, CA, USA: IEEE Computer Society. doi: 10.1109/QEST.2007.18
Zafar, Saad, Colvin, Robert, Winter, Kirsten, Yatapanage, Nisansala and Dromey, R.G. (2007). Early validation and verification of a distributed role-based access control model. APSEC 2007: 14th Asia-Pacific Software Engineering Conference 2007, Nagoya, Japan, 5-7 December 2007. Piscataway, NJ, United States: IEEE Computer Society. doi: 10.1109/ASPEC.2007.20
Colvin, R. and Groves, L. (2007). A scalable lock-free stack algorithm and its verification. Fifth IEEE International Conference on Software Engineering and Formal Methods, London, United Kingdom, 12-14 September 2007. Los Alamitos, CA, United States: IEEE Computer Society. doi: 10.1109/SEFM.2007.2
Grunske, Lars, Winter, Kirsten and Colvin, Robert (2007). Timed behavior trees and their application to verifying real-time systems. Australian Conference on Software Engineering (ASWEC 2007), Melbourne, Australia, 10-13 April 2007. Washington, DC, USA: IEEE Computer Society. doi: 10.1109/ASWEC.2007.49
Colvin, Robert and Dongol, Brijesh (2007). Verifying lock-freedom using well-founded orders. Theoretical Aspects of Computing - ICTAC 2007, Macau, China, 26-28 September, 2007. Heidelberg, Germany: Springer. doi: 10.1007/978-3-540-75292-9_9
Colvin, Robert, Groves, Lindsay, Luchangco, Victor and Moir, Mark (2006). Formal verification of a lazy concurrent list-based set algorithm. 18th International Conference on Computer Aided Verification (CAV 2006), Seattle, WA, USA, 17-20 August, 2006. Berlin, Germany: Springer-Berlin. doi: 10.1007/11817963_44
Colvin, Robert, Doherty, Simon and Groves, Lindsay (2005). Verifying concurrent data structures by simulation. REFINE 2005 Workshop, Guildford, England, UK, April, 2005. Amsterdam, Netherlands: Elsevier. doi: 10.1016/j.entcs.2005.04.026
Colvin, Robert and Groves, Lindsay (2005). Formal verification of an array-based nonblocking queue. ICECCS 2005: Engineering of Complex Computer Systems, Shanghai, China, 16-20 June 2005. Piscataway, NJ, United States: IEEE. doi: 10.1109/ICECCS.2005.49
Colvin, Robert, Hayes, Ian J., Hemer, David G. and Strooper, Paul A. (2003). Refinement of higher-order logic programs. The Twelfth International Symposium on Logic-based Program Synthesis and Transformation, Madrid, Spain, 17-20 September 2002. Berlin: Springer. doi: 10.1007/3-540-45013-0_11
Hemer, David, Colvin, Robert, Hayes, Ian and Strooper, Paul (2002). Don't care non-determinism in logic program refinement. CATS'02, Computing: the Australasian Theory Symposium, Amsterdam, Denmark, 28 January - 1 February 2002. Amsterdam ; New York: Elsevier Science. doi: 10.1016/S1571-0661(04)00308-1
Colvin, R., Hayes, I. J., Hemer, D. G. and Strooper, P. A. (2002). Translating refined logic programs to Mercury. ACSC 2002, Melbourne, Australia, 28 January - 1 February, 2002. Sydney, Australia: Australian Computer Society Inc..
Colvin, 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
Colvin, 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
Colvin, R., Hayes, I. J. and Strooper, P. (1998). Data refining logic programs. International Refinement Workshop and Formal Methods Pacific '98, Canberra, Australia, 29 September - 2 October, 1998. New York: Springer -Verlag.
Colvin, R., Hayes, I., Nickson, R. and Strooper, P. (1997). A tool for logic program refinement (Extended abstract). Formal Methods Pacific Conference (FMP 97), Wellington New Zealand, 9-11 July 1997. Singapore: Springer-Verlag Singapore Pte..
Working Paper
Colvin, Robert (2013). Modeling neural networks using process algebras. Queensland Brain Institute, The University of Queensland.
Thesis
Colvin, Robert John (2002). Contextual and data refinement for the refinement calculus for logic programs. PhD Thesis, School of Information Technology and Electrical Engineering, The University of Queensland. doi: 10.14264/106036
Department Technical Reports
Lindsay, Peter A., Winter, Kirsten and Colvin, Robert (2010). Model-checking tool support for quantitative risk analysis and design for safety. Division of Systems and Software Engineering Research, Technical Report SSE-2010-04. School of Information Technolology and Electrical Engineering, The University of Queensland.
Colvin, Robert and Hayes, Ian J. (2010). A semantics for behavior trees. Systems and Software Engineering Technical Reports, SSE-2010-03. School of Information Technol and Elec Engineering, University of Queensland.
Colvin, Robert and Hayes, Ian J. (2010). Structural operational semantics through context-dependent behaviour. Systems and Software Engineering Technical Reports, SSE-2010-02. School of Information Technology and Electrical Engineering, The University of Queensland.
Colvin, Robert, Hemer, David, Hayes, Ian and Strooper, Paul (2001). Translating Refined Logic Programs to Mercury. Technical Report no. 01-32. Software Verification Research Centre, School of Information Technology, The University Of Queensland.
Hemer, D. G., Colvin, R., Hayes, I. J. and Strooper, P. A. (2001). Don't care non-determinism in logic program refinement. SRV Techical Report No. 01-27. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Hayes, Ian, Nickson, Ray, Strooper, Paul and Colvin, Robert (2000). A Declarative Semantics for Logic Program Refinement. Technical Report no. 00-30. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Colvin, 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.