The University of Queensland

Practical model-based testing

Utting, Mark and Legeard, Bruno (2007). Practical model-based testing. Amsterdam, Netherlands: Elsevier. doi: 10.1016/b978-0-12-372501-1.x5000-5

Practical model-based testing: A tools approach

Utting, Mark and Legeard, Bruno (2006). Practical model-based testing: A tools approach. Elsevier. doi: 10.1016/B978-0-12-372501-1.X5000-5

Pipeline specification of a MIPS R3000 CPU

Utting, Mark and Kearney, Peter (1994). Pipeline specification of a MIPS R3000 CPU. SVRC Technical Report, 92-6. Software Verification Research Centre, Department of Computer Science, The University of Queensland.

Real time behaviour of a RISC processor: specification and computer-aided verification

Kearney, Peter, Utting, Mark and Whitwell, Keith (1994). Real time behaviour of a RISC processor: specification and computer-aided verification. SVRC Technical Report, 92-10. Software Verification Research Centre, Department of Computer Science, The University of Queensland.

Specification issues for real-time behaviour of RISC processors

Utting, Mark and Kearney, Peter (1992). Specification issues for real-time behaviour of RISC processors. SVRC Technical Report, 92-5. Software Verification Research Centre, Department of Computer Science, The University of Queensland.

Recent advances in model-based testing

Utting, Mark, Legeard, Bruno, Bouquet, Fabrice, Fourneret, Elizabeta, Peureux, Fabien and Vernotte, Alexandre (2016). Recent advances in model-based testing. Advances in Computers. (pp. 53-120) edited by Atif Memon. Cambridge, MA, United States: Academic Press. doi: 10.1016/bs.adcom.2015.11.004

How to design extended finite state machine test models in Java

Utting, Mark (2011). How to design extended finite state machine test models in Java. Model-based testing for embedded systems. (pp. 1-24) Boca Raton, FL, United States: CRC Press. doi: 10.1201/b11321-7

Deadlines are termination

Hayes, I. J. and Utting, M. (1998). Deadlines are termination. Programming Concepts and Methods PROCOMET ’98. (pp. 186-204) Boston, MA, United States: Springer. doi: 10.1007/978-0-387-35358-6_15

Verifying Whiley programs with Boogie

Pearce, David J., Utting, Mark and Groves, Lindsay (2022). Verifying Whiley programs with Boogie. Journal of Automated Reasoning, 66 (4), 1-57. doi: 10.1007/s10817-022-09619-1

Automatic proofs of memory deallocation for a Whiley-to-C Compiler

Weng, Min-Hsien, Malik, Robi and Utting, Mark (2021). Automatic proofs of memory deallocation for a Whiley-to-C Compiler. Formal Methods in System Design, 57 (3), 429-472. doi: 10.1007/s10703-021-00378-0

Impact of technology uptake on an Australian electricity distribution network

Boulaire, Fanny, Utting, Mark and Drogemuller, Robin (2015). Impact of technology uptake on an Australian electricity distribution network. Environmental Modelling and Software, 69, 196-213. doi: 10.1016/j.envsoft.2015.03.019

Dynamic agent composition for large-scale agent-based models

Boulaire, Fanny, Utting, Mark and Drogemuller, Robin (2015). Dynamic agent composition for large-scale agent-based models. Complex Adaptive Systems Modeling, 3 (1) 1. doi: 10.1186/s40294-015-0007-2

The JStar language philosophy

Utting, Mark, Weng, Min-Hsien and Cleary, John G. (2014). The JStar language philosophy. Parallel Computing, 40 (SI2), 35-50. doi: 10.1016/j.parco.2013.11.004

A taxonomy of model-based testing approaches

Utting, Mark, Pretschner, Alexander and Legeard, Bruno (2012). A taxonomy of model-based testing approaches. Software Testing Verification and Reliability, 22 (5), 297-312. doi: 10.1002/stvr.456

Evolving web-based test automation into agile business specifications

Mugridge, Rick, Utting, Mark and Streader, David (2011). Evolving web-based test automation into agile business specifications. Future Internet, 3 (2), 159-174. doi: 10.3390/fi3020159

Un panorama du test à partir de modèles formels

Utting, Mark (2006). Un panorama du test à partir de modèles formels. Techniques et sciences informatiques, 25 (1), 133-139. doi: 10.3166/tsi.25.133-139

Requirements traceability in automated test generation: application to smart card software validation

Bouquet, F., Jaffuel, E., Legeard, B., Peureux, F. and Utting, M. (2005). Requirements traceability in automated test generation: application to smart card software validation. ACM SIGSOFT Software Engineering Notes, 30 (4), 1-7. doi: 10.1145/1082983.1083282

Controlling test case explosion in test generation from B formal models

Legeard, Bruno, Peureux, Fabien and Utting, Mark (2004). Controlling test case explosion in test generation from B formal models. Software Testing Verification and Reliability, 14 (2), 81-103. doi: 10.1002/stvr.287

ERGO 6: A generic proof engine that uses prolog proof technology

Utting, M., Robinson, P. J. and Nickson, R. (2002). ERGO 6: A generic proof engine that uses prolog proof technology. Journal of Computation and Mathematics, 5, 194-219. doi: 10.1112/s1461157000000759

Teaching formal methods lite via testing

Utting, Mark and Reeves, Steve (2001). Teaching formal methods lite via testing. Software Testing Verification and Reliability, 11 (3), 181-195. doi: 10.1002/stvr.223

A sequential real-time refinement calculus

Hayes, I. J. and Utting, M. (2001). A sequential real-time refinement calculus. Acta Informatica, 37 (6), 385-448. doi: 10.1007/PL00013311

A formal method for building concurrent real-time software

Fidge, Colin, Kearney, Peter and Utting, Mark (1997). A formal method for building concurrent real-time software. IEEE Software, 14 (2), 99-106. doi: 10.1109/52.582979

EVM-Vale: formal verification of EVM bytecode using vale

Cumming, Daniel, Utting, Mark, Cassez, Franck, Dong, Naipeng, Bayat Tork, Sadra and Risius, Marten (2024). EVM-Vale: formal verification of EVM bytecode using vale. 7th International Symposium, SDLT 2023, Brisbane, QLD, Australia, 30 November - 1 December 2023. Heidelberg, Germany: Springer. doi: 10.1007/978-981-97-0006-6_3

Differential testing of a verification framework for compiler optimizations (Case study)

Utting, Mark, Webb, Brae J. and Hayes, Ian J. (2023). Differential testing of a verification framework for compiler optimizations (Case study). IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), Melbourne, VIC Australia, 14-15 May 2023. Piscataway, NJ United States: Institute of Electrical and Electronics Engineers.. doi: 10.1109/formalise58978.2023.00015

TypeScript’s evolution: an analysis of feature adoption over time

Scarsbrook, Joshua D., Utting, Mark and Ko, Ryan K. L. (2023). TypeScript’s evolution: an analysis of feature adoption over time. IEEE/ACM 20th International Conference on Mining Software Repositories (MSR), Melbourne, VIC, Australia, 15-16 May 2023. Piscataway, NJ, United States: IEEE. doi: 10.1109/msr59073.2023.00027

Verifying term graph optimizations using Isabelle/HOL

Webb, Brae J., Hayes, Ian J. and Utting, Mark (2023). Verifying term graph optimizations using Isabelle/HOL. 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'23), Boston, MA, United States, 16-17 January 2023. New York, NY, United States: ACM. doi: 10.1145/3573105.3575673

Verifying compiler optimisations (invited paper)

Hayes, Ian J., Utting, Mark and Webb, Brae J. (2023). Verifying compiler optimisations (invited paper). 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, 21–24 November 2023. Singapore, Singapore: Springer Nature Singapore. doi: 10.1007/978-981-99-7584-6_1

Verification of EVM Bytecode with Vale

Cumming, Daniel Keith, Utting, Mark, Dong, Naipeng, Cassez, Frank, Tork, S. B. and Risius, Marten (2022). Verification of EVM Bytecode with Vale. 6th Symposium on Distributed Ledger Technology 2022 (SDLT 2022), Gold Coast, QLD Australia, 22 November 2022.

A formal semantics of the GraalVM intermediate representation

Webb, Brae J., Utting, Mark and Hayes, Ian J. (2021). A formal semantics of the GraalVM intermediate representation. 19th International Symposium, ATVA 2021, Gold Coast, QLD Australia, 18-22 October 2021. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-030-88885-5_8

Tool support for refactoring manual tests

Bernard, Elodie, Botella, Julien, Ambert, Fabrice, Legeard, Bruno and Utting, Mark (2020). Tool support for refactoring manual tests. 2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST), Porto, Portugal, 24-28 October 2020. Piscataway, NJ, United States: Institute of Electrical and Electronics Engineers. doi: 10.1109/icst46399.2020.00041

Identifying and generating missing tests using machine learning on execution traces

Utting, Mark, Legeard, Bruno, Dadeau, Frederic, Tamagnan, Frederic and Bouquet, Fabrice (2020). Identifying and generating missing tests using machine learning on execution traces. IEEE International Conference on Artificial Intelligence Testing (AITest), Oxford, United Kingdom, 3-6 August 2020. Piscataway, NJ, United States: IEEE. doi: 10.1109/aitest49225.2020.00020

An introduction to software verification with Whiley

Pearce, David J., Utting, Mark and Groves, Lindsay (2019). An introduction to software verification with Whiley. Third International School, SETSS 2017, Chongqing, China, 17-22 April 2017. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-030-17601-3_1

Making Whiley boogie!

Utting, Mark, Pearce, David J. and Groves, Lindsay (2017). Making Whiley boogie!. 13th International Conference, Integrated Formal Methods 2017, Turin, Italy, 20 - 22 September 2017. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-319-66845-1_5

Static techniques for reducing memory usage in the C implementation of Whiley programs

Weng, Min-Hsien, Pfahringer, Bernhard and Utting, Mark (2017). Static techniques for reducing memory usage in the C implementation of Whiley programs. ACSW '17: Australasian Computer Science Week Multiconference, Geelong, VIC Australia, January 30-February 03, 2017. New York, NY USA: ACM Press. doi: 10.1145/3014812.3014827

Bound Analysis for Whiley Programs

Weng, Min-Hsien, Utting, Mark and Pfahringer, Bernhard (2016). Bound Analysis for Whiley Programs. Amsterdam, Netherlands: Elsevier. doi: 10.1016/j.entcs.2016.01.005

Aggregating energy supply and demand

Drogemuller, R, Boulaire, F, Ledwich, G, Buys, L, Utting, M, Vine, D, Morris, P and Arefi, A (2014). Aggregating energy supply and demand. ECPPM 2014, 10th European Conference on Product and Process Modelling, Vienna, Austria, 17-19 September 2014. London, United Kingdom: CRC Press. doi: 10.1201/b17396-71

Parallel ABM for electricity distribution grids: a case study

Boulaire, Fanny, Utting, Mark and Drogemuller, Robin (2014). Parallel ABM for electricity distribution grids: a case study. Euro-Par 2013: Parallel Processing Workshops, Aachen, Germany, 26 - 27 August 2013. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/978-3-642-54420-0_55

MODAM: a modular agent-based modelling framework

Boulaire, Fanny, Utting, Mark and Drogemuller, Robin (2013). MODAM: a modular agent-based modelling framework. 2nd International Workshop on Software Engineering Challenges for the Smart Grid (SE4SG), San Francisco, CA USA, 18 May 2013. Piscataway, NJ USA: Institute of Electrical and Electronics Engineers. doi: 10.1109/SE4SG.2013.6596109

The JStar language philosophy

Utting, Mark, Weng, Min-Hsien and Cleary, John G. (2013). The JStar language philosophy. 2013 International Workshop on Programming Models and Applications for Multicores and Manycores, Shenzhen, China, 23 February 2013. New York, NY USA: The Association for Computing Machinery . doi: 10.1145/2442992.2442996

A hybrid simulation framework to assess the impact of renewable generators on a distribution network

Boulaire, Fanny, Utting, Mark, Drogemuller, Robin, Ledwich, Gerard and Ziari, Iman (2012). A hybrid simulation framework to assess the impact of renewable generators on a distribution network. 2012 Winter Simulation Conference, Berlin, Germany, 9-12 December 2012. doi: 10.1109/WSC.2012.6465000

Transformation rules for Z

Utting, Mark, Malik, Petra and Toyn, Ian (2009). Transformation rules for Z.

Putting formal specifications under the magnifying glass: Model-based testing for validation

Aydal, Emine G., Paige, Richard F., Utting, Mark and Woodcock, Jim (2009). Putting formal specifications under the magnifying glass: Model-based testing for validation. doi: 10.1109/ICST.2009.20

The role of model-based testing

Utting, Mark (2008). The role of model-based testing. doi: 10.1007/978-3-540-69149-5_56

Unit testing of Z specifications

Utting, Mark and Malik, Petra (2008). Unit testing of Z specifications. doi: 10.1007/978-3-540-87603-8_24

A comparison of state-based modelling tools for model validation

Aydal, Emine G., Utting, Mark and Woodcock, Jim (2008). A comparison of state-based modelling tools for model validation. 46th International Conference, TOOLS EUROPE 2008: Objects, Components, Models and Patterns, Zurich, Switzerland, June/July 2008. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/978-3-540-69824-1_16

A subset of precise UML for model-based testing

Bouquet, F., Grandpierre, C., Legeard, B., Peureux, F., Vacelet, N. and Utting, M. (2007). A subset of precise UML for model-based testing. New York, NY, USA: ACM. doi: 10.1145/1291535.1291545

Jumble java byte code to measure the effectiveness of unit tests

Irvine, Sean A., Pavlinic, Tin, Trigg, Leonard, Cleary, John G., Inglis, Stuart and Utting, Mark (2007). Jumble java byte code to measure the effectiveness of unit tests. Mutation 2007 Conference, Windsor England, Sep 10-14, 2007. LOS ALAMITOS: IEEE. doi: 10.1109/TAICPART.2007.4344121

Model-based testing from UML models

Bernard, Eddy, Bouquet, Fabrice, Charbonnier, Amandine, Legeard, Bruno, Peureux, Fabien, Utting, Mark and Torreborre, Eric (2006). Model-based testing from UML models.

CZT support for Z extensions

Miller, Tim, Freitas, Leo, Malik, Petra and Utting, Mark (2005). CZT support for Z extensions. IFM 2005: Integrated Formal Methods, Eindhoven, The Netherlands, 29 November - 2 December 2005. Berlin, Germany: Springer. doi: 10.1007/11589976_14

CZT: a framework for Z tools

Malik, Petra and Utting, Mark (2005). CZT: a framework for Z tools. ZB 2005: ZB 2005: Formal Specification and Development in Z and B, Guildford, United Kingdom, 13 - 15 April 2005. Berlin, Germany: Springer. doi: 10.1007/11415787_5

JML-testing-tools: a symbolic animator for JML specifications using CLP

Bouquet, Fabrice, Dadeau, Frédéric, Legeard, Bruno and Utting, Mark (2005). JML-testing-tools: a symbolic animator for JML specifications using CLP. TACAS 2005: Tools and Algorithms for the Construction and Analysis of Systems, Edinburgh, United Kingdom, 4 - 8 April 2005. Heidelberg, Germany: Springer. doi: 10.1007/978-3-540-31980-1_37

Requirements traceability in automated test generation: application to smart card software validation

Bouquet, F., Jaffuel, E., Legeard, B., Peureux, F. and Utting, M. (2005). Requirements traceability in automated test generation: application to smart card software validation. A-MOST '05: 1st international workshop on Advances in model-based testing, St Louis, MO, United States, 15 - 16 May 2005. New York, NY, United States: Association for Computing Machinery. doi: 10.1145/1083274.1083282

Symbolic animation of JML specifications

Bouquet, Fabrice, Dadeau, Frédéric, Legeard, Bruno and Utting, Mark (2005). Symbolic animation of JML specifications. FM 2005: FM 2005: Formal Methods, Newcastle, United Kingdom, 18 - 22 July 2005. Heidelberg, 69121 Germany: Springer. doi: 10.1007/11526841_7

Boundary coverage criteria for test generation from formal models

Kosmatov, Nikolai, Legeard, Bruno, Peureux, Fabien and Utting, Mark (2004). Boundary coverage criteria for test generation from formal models. IEEE Computer Society. doi: 10.1109/issre.2004.12

Faster analysis of formal specifications

Bouquet, Fabrice, Legeard, Bruno, Utting, Mark and Vacelet, Nicolas (2004). Faster analysis of formal specifications. ICFEM 2004: Formal Methods and Software Engineering, Seattle, WA, United States, 8 - 12 November 2004. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/978-3-540-30482-1_24

Object orientation without extending Z

Utting, Mark and Wang, Shaochun (2003). Object orientation without extending Z. ZB 2003: Formal Specification and Development in Z and B, Turku, Finland, 4 - 6 June 2003. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-44880-2_20

Tabling structures for bottom-up logic programming

Clayton, Roger, Cleary, John G., Pfahringer, Bernhard and Utting, Mark (2003). Tabling structures for bottom-up logic programming. LOPSTR 2002: Logic Based Program Synthesis and Transformation, Madrid, Spain, September 2002. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-45013-0_5

ZML: XML support for standard Z

Utting, Mark, Toyn, Ian, Sun, Jing, Martin, Andrew, Dong, Jin Song, Daley, Nicholas and Currie, David (2003). ZML: XML support for standard Z. ZB 2003: ZB 2003: Formal Specification and Development in Z and B, Turku, Finland, 4 - 6 June 2003. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-44880-2_26

A comparison of the BTT and TTF test-generation methods

Legeard, Bruno, Peureux, Fabien and Utting, Mark (2002). A comparison of the BTT and TTF test-generation methods. ZB 2002: ZB 2002:Formal Specification and Development in Z and B, Grenoble, France, 23 - 25 January 2002. Berlin, Germany: Springer Verlag. doi: 10.1007/3-540-45648-1_16

Automated boundary testing from Z and B

Legeard, Bruno, Peureux, Fabien and Utting, Mark (2002). Automated boundary testing from Z and B. FME 2002: FME 2002:Formal Methods—Getting IT Right, Copenhagen, Denmark, 22 - 24 July 2002. Berlin, Germany: Springer Verlag. doi: 10.1007/3-540-45614-7_2

A survey of software development practices in the New Zealand software industry

Groves, Lindsay, Nickson, Ray , Reeve, Greg, Reeves, Steve and Utting, Mark (2000). A survey of software development practices in the New Zealand software industry. 2000 Australian Software Engineering Conference, Canberra, ACT, Australia, 28 - 29 April 2000. Piscataway, NJ, United States: Institute of Electrical and Electronics Engineers. doi: 10.1109/aswec.2000.844576

A real-time refinement calculus that changes only time

Utting, Mark and Fidge, Colin (1996). A real-time refinement calculus that changes only time. BCS-FACS 7th Refinement Workshop, Bath, United Kingdom, 3 - 5 July 1996. United Kingdom: British Computer Society Learning & Development. doi: 10.14236/ewic/rw1996.14

Coercing real-time refinement: a transmitter

Hayes, Ian and Utting, Mark (1996). Coercing real-time refinement: a transmitter. BCS-FACS Northern Formal Methods Workshop, Ilkley, United Kingdom, 23-24 September 1996. BCS Learning & Development. doi: 10.14236/ewic/fa1996.9

Integrating real-time scheduling theory and program refinement

Fidge, C., Utting, M., Kearney, P. and Hayes, I. (1996). Integrating real-time scheduling theory and program refinement. 3rd International Symposium of Formal Methods Europe, FME 1996, Oxford, United Kingdom, 18-22 March 1996. Springer Verlag. doi: 10.1007/3-540-60973-3_95

Interactively verifying a simple real-time scheduler

Fidge, Colin, Kearney, Peter and Utting, Mark (1995). Interactively verifying a simple real-time scheduler. CAV 1995: Computer Aided Verification, Liège, Belgium, 3-5 July 1995. Heidelberg, Germany: Springer. doi: 10.1007/3-540-60045-0_65

Animating Z: Interactivity, transparency and equivalence

Utting, M. (1995). Animating Z: Interactivity, transparency and equivalence. 1995 Asia Pacific Software Engineering Conference, Brisbane, QLD, Australia, 6-9 December 1995. Piscataway, NJ, United States: Institute of Electrical and Electronics Engineers. doi: 10.1109/APSEC.1995.496978

Interactively verifying a simple real-time scheduler

Fidge C., Kearney P. and Utting M. (1995). Interactively verifying a simple real-time scheduler. 7th International Conference on Computer Aided Verification, CAV 1995, Liège, Belgium, 3 - 5 July 1995. Cham, Switzerland: Springer Verlag.

A layered real-time specification of a RISC processor

Kearney, Peter and Utting, Mark (1994). A layered real-time specification of a RISC processor. FTRTFT 1994, ProCoS 1994: Formal Techniques in Real-Time and Fault-Tolerant Systems, Lübeck, Germany, 19 - 23 September 1994. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-58468-4_178

Modular reasoning in an object-oriented refinement calculus

Utting, Mark and Robinson, Ken (1993). Modular reasoning in an object-oriented refinement calculus. MPC 1992: Mathematics of Program Construction, Oxford, United Kingdom, 29 June - 3 July 1992. Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-56625-2_22

A tactic driven refinement tool

Groves, Lindsay, Nickson, Raymond and Utting, Mark (1992). A tactic driven refinement tool. 5th Refinement Workshop, London, United Kingdom, 8 - 10 January 1992. London, United Kingdom: Springer London. doi: 10.1007/978-1-4471-3550-0_14

Discussion Paper: 2023-2030 Australian Cyber Security Strategy

Abeysooriya, Sasenka, Akhlaghpour, Saeed, Bongiovanni, Ivano, Dowsett, Dallas, Grotowski, Joseph, Holm, Mike, Kim, Dan, Ko, Ryan, Phillips, Andelka M., Slapnicar, Sergeja, Stockdale, David, Swinson, John, Thonon, Geoffroy, Utting, Mark, Walker-Munro, Brendan and Willoughby, Shannon (2023). Discussion Paper: 2023-2030 Australian Cyber Security Strategy. UQ CYBER and AUSCERT.

Method of evaluating genomic sequences

Cleary, John Gerald and Utting, Barry Mark (2015). Method of evaluating genomic sequences. US9165253B2.

Deadlines are termination

Hayes, Ian J. and Utting, Mark (1998). Deadlines are termination. Technical Report 98-01 St Lucia, QLD, Australia: Software Verification Research Centre, School of Information Technology, The University of Queensland.