The 24th International Conference on Formal Engineering Methods


21 - 24 November 2023 - Brisbane, Australia (Physical)

Welcome to the website of the 24th International Conference on Formal Engineering Methods (ICFEM 2023)

ICFEM is an international leading conference series in formal methods and software engineering. Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, present their research, and help advance the state of the art. ICFEM is interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM has been hosted in many countries around the world.

ICFEM 2024 will be hosted in Hiroshima, Japan.

Scope and Topics

Authors are invited to submit high quality technical papers describing original and unpublished work in all theoretical aspects of software engineering. Topics of interest include, but are not limited to:

  • Abstraction, refinement and evolution
  • Formal specification and modelling
  • Formal verification and analysis
  • Model checking and equivalence checking
  • Automated and interactive theorem proving
  • Formal approaches to software testing and inspection
  • Formal methods for self-adaptive systems
  • Formal methods for object-oriented systems
  • Formal methods for component-based systems
  • Formal methods for concurrent and real-time systems
  • Formal methods for cloud computing
  • Formal methods for cyber-physical systems
  • Formal methods for hardware and embedded systems
  • Formal methods for software safety and security
  • Formal methods for software reliability and dependability
  • Development, integration and experiments involving verified systems
  • Formal certification of products under international standards
  • Formal model-based development and code generation

Registration

Student Early
(until 05 Oct)		 General Early
(until 05 Oct)		 Student Standard
(after 05 Oct)		 General Standard
(after 05 Oct)
ICFEM All Package* 1077 AUD (≈ 730 USD) 1254 AUD (≈ 850 USD) 1254 AUD (≈ 850 USD) 1430 AUD (≈ 970 USD)
ICFEM Only** 960 AUD (≈ 650 USD) 1150 AUD (≈ 780 USD) 1150 AUD (≈ 780 USD) 1327 AUD (≈ 900 USD)
Workshops/Doc Symp*** 192 AUD (≈ 130 USD) 265 AUD (≈ 180 USD) 265 AUD (≈ 180 USD) 340 AUD (≈ 230 USD)

Note that authors' registration deadline is the same as the early bird deadline (05 Oct 2023).

*ICFEM All Package includes ICFEM conference, all the workshops, doctoral symposium, morning tea, lunch, afternoon tea every day (4 days) and a conference dinner.

**ICFEM Only includes ICFEM conference, morning tea, lunch, afternoon tea every day (3 days) and a conference dinner.

***Workshops/Doc Symp includes workshops OR the doctoral symposium, morning tea, lunch, and afternoon tea (1 day).

The USD conversion is only for indication purposes. The attendants should use the AUD price for registration.

Due to tax issues, residents in Australia will go through a different payment process, so please choose the following links accordingly. The fees are the same.


If you do not live in Australia, please use the following link to register.
Overseas Delegates Register here


If you live in Australia, please use the following link to register.
Australian Delegates Register here

Visa Application

To help attendees prepare the visa letter, please email mengyao.ma@uq.edu.au.

General information for Australian visa applicants can be found here. Business conference visa information can be found here. Further information about the specific requirements of Visitor visas is available on the Department's website.

Venue and Accomodation

The 24th International Conference on Formal Engineering Methods (ICFEM 2023) will take place in Novotel Brisbane South Bank.

Novotel Brisbane South Bank contemporary hotel is perfectly placed in the heart of the South Bank Parklands. Adjacent to the hotel is seven hectares of luscious grass at Musgrave Park, which hosts some of Brisbane's vibrant annual festivals and events. Take a short walk to the Brisbane Convention and Exhibition Centre. Beyond the Centre, you'll enjoy stunning views, lush parklands, superb dining experiences, vibrant art galleries, riverbank Streets Beach and world class shopping in the Brisbane CBD shopping district.

Novotel Brisbane South Bank has provided ICFEM 2023 with up to 20% discount on accommodation. Book online with the link here to get the discounted rate. The offer is valid until 6th Nov, and exclusive for 19th-24th Nov. If the you would like to extend booking further, please contact the hotel directly via HA0X0@accor.com or call +61 (07) 3295 4100.

Alternative Accommodations

40 Elizabeth Street, Brisbane City QLD 4000

ibis Styles Brisbane Elizabeth Street has provided ICFEM 2023 with about 15% discount on accommodation. Book online with the link here to get the discounted rate. The offer is valid for stay from Friday, 17th November through to Monday, 27th November inclusive.

Located in the heart of the Brisbane CBD, the 367 room ibis Styles Brisbane features uninterrupted views of Brisbane River and the South Bank cultural precinct. Vibrant colours and playful design extend through the lobby, to the Social Restaurant and Bar, while rooms blend comfort, connectivity and style. The best shopping and dining in Brisbane is at its doorstep with access to Queen Street Mall, Treasury Casino, Eagle Street Pier, Convention Centre and public transportation.

218 Vulture St, South Brisbane QLD 4101

Courtyard Brisbane South Bank has provided ICFEM 2023 with about 15% discount on accommodation. Book online with the link here to get the discounted rate. The offer is valid for stay from Friday, 17th November through to Monday, 27th November inclusive.

Set on the fringe of the Brisbane CBD, Courtyard Brisbane South Bank offers an ideal location near the South Bank Parklands in Brisbane, Australia. Experience everything the vibrant state of Queensland has to offer from this family friendly hotel. It is just steps away from public transport options for easy travel to world class eateries, shops, gardens and entertainment venues. Before you begin your day in South Brisbane energize with a workout in the 24-hr fitness centre or take a swim in the heated indoor pool.

267 Grey St, South Brisbane QLD 4101

Emporium Hotel South Bank has provided ICFEM 2023 with about 10-15% discount on accommodation. The discount is automatically applied when guests enter their dates on the website.

A spectacular new standard in exquisite boutique luxury accommodation and award-winning service. 143 luxuriously appointed suites feature all the comforts you could ask for, while an abundance of premium food and beverage options will leave you spoilt for choice. On level 21 you will find a spectacular, 23m infinity edge pool and bar with magnificent views over South Bank Parklands, the Brisbane River, to the city and beyond. The coveted north easterly aspect will allow comfort and enjoyment morning to night, all year round.

Program

Download the program here.

Keynote Speakers

Graeme Smith is an Associate Professor of Computer Science at The University of Queensland and Principal Scientist of the Defence Science and Technology Group (Australia). Prior to his current position he held research positions with the Software Verification Research Centre (Australia), GMD First (Germany), the Technical University of Berlin, and the Centre de Recherche en Informatique de Nancy (France). His research interests are in the application of formal techniques to functional correctness and security of concurrent systems. His most recent work focuses on how the effects of compiler and hardware optimisations on concurrent programs interact with information flow security.

Title: Compositional reasoning at the software/hardware interface

Abstract:

Rely/guarantee reasoning provides a compositional approach to reasoning about multi-threaded programs. It is sound under the assumption that the individual threads execute in a sequentially consistent manner. However, this is not the case on modern multicore processors which routinely employ out-of-order execution for efficiency gains. This loss of sequential consistency has no effects on the functionality of high-level programs that are data-race free, and for those programs rely/guarantee reasoning remains sound. However, this is not the case for code developed to include data races for efficiency, such as operating system routines and programming library data structures - the code on which much of our software depends.

In this talk, I will explain the effects of out-of-order execution on such code and how soundness of rely/guarantee reasoning can be restored by using additional checks. I will also look at how these checks apply to reasoning about low-level security vulnerabilities, such as Spectre.

Yuxi Fu is a professor of the Department of Computer Science, Shanghai Jiao Tong University. His research interest is in theoretical computer science. His publications cover topics in type theory, semantics, concurrency theory, theory of interaction, equivalence checking. He developed theory of interaction as a general theory that gives a uniform account of both computation models and interaction models. The theory is based on Thesis on Interaction, which is an interactive version of Thesis on Computation (Church-Turing Thesis). The overall goal of the general model theory is to provide a model independent foundation for both the programming theory and the computing theory. In the area of equivalence checking, he has solved a number of open problems, including the decidability of branching bisimilarity for BPA, the decidability of the branching bisimilarity of the epsilon-pushing PDA and epsilon-popping PDA. Currently his main focus is on the complexity of VASS reachability.

Title: A Theory for Interaction

Abstract:

A general theory for interaction is outlined. The theory features a model independent appraoch to concurrency and process models. Within the framework equality theory, expressiveness theory are studied. And a Thesis for Interaction is proposed as the foundation for interaction theory.

Yamine AIT AMEUR is Full Professor since 2000. Since Sept 2011, he is at Toulouse INP (National Polytechnique Institute) in Toulouse (France) and member of the Toulouse research institute in computing (IRIT-CNRS). Two main important aspects characterize his research activities. On the one hand the fundamental aspects through the development and use of state based formal modelling techniques based on refinement and proofs, in particular Event-B and explicit formalisation of the semantics of domain knowledge using formalised ontology models. On the other, hand, practical aspects, through the development of operational applications, allowing to validate the proposed approaches. Embedded systems in avionics, engineering, interactive systems, CO2 capture are some of the application domains targeted by this work

Title: Separation of Concerns for Complexity Mitigation in System and Domain Formal Modelling – A Dive into Algebraic Event-B Theories

Abstract:

Formal methods have shown their ability and efficiency in the design, analysis and verification of safety critical complex software systems. A crucial challenge for formal methods nowadays is to make them reasonably accessible, as to foster a wider adoption across system engineering, and make their implementation and deployment more operational for non-expert engineers and researchers alike. From our point of view, promoting the reuse and sharing of explicitly formalised elements such as models, theories, proofs, etc. contributes, undoubtedly, to the dissemination of these methods. As a result, reuse mechanisms must be defined and integrated into development processes such as refinement, abstraction, composition/decomposition, etc.

In this talk, we will discuss state -based formal methods, namely the Event-B method. We report on our findings about the definition of algebraic theories that are utilised within Event-B model refinement chains. In our method, Event-B models borrow operators, axioms, theorems, proof and rewrite rules from these theories. Relying on their well-definedness, these operators, axioms, theorems and proof and rewrite rules are useful to discharge the proof obligations generated for these models, and contribute to reducing development efforts, as theorems of the theories are proved once and for all. The approach is illustrated on the generation of new proof obligations and on system models conformance to engineering standards.

Invited Talks

Ian Hayes
The University of Queensland, Australia
Verifying Compiler Optimisations
Toby Murray
University of Melbourne, Australia
Practical Verified Concurrent Program Security
Dirk Pattinson
The Australian National University, Australia
Certified Proof and Non-Provability
Subodh Sharma
Indian Institute of Technology Delhi, India
On Analysing Weak Memory Concurrency

Proceedings

Please refer to the ICFEM 2023 proceedings.

Affiliated Events

The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (FAVPQC 2023), 21 November 2023

The 7th Symposium on Distributed Ledger Technology (SDLT 2023), 21 - 22 November 30 November - 1 December 2023

Attractions

Welcome to Brisbane, Australia's thriving subtropical capital city situated in the heart of the Sunshine State, Queensland. As the third-largest city in Australia, Brisbane offers a dynamic fusion of urban sophistication, natural beauty, and a rich cultural scene.

Queensland Art Gallery, located in Brisbane, is famous for its extensive collection of Australian and Indigenous art, diverse international exhibits, and striking modern architecture. It's a must-visit for art lovers, and its beautiful riverside setting offers a unique cultural experience in the heart of the city.
The Brisbane River offers endless adventure and leisure opportunities, from kayaking and paddleboarding to City Cat rides and picnics in riverside parks. You can enjoy stunning views from Kangaroo Point Cliffs, try rock climbing or abseiling with Riverlife Adventure Centre, and even explore the Story Bridge.
The Queensland Museum showcases Queensland's natural history, cultural heritage, and scientific achievements through a mix of permanent and rotating exhibitions that connect visitors to the state's rich history and global impact, making it a dynamic destination for learning and exploration.
In Lone Pine Koala Sanctuary, discover over 70 species of Australian native animals in a beautiful, natural bush setting at the world's first and largest koala sanctuary. Meet a koala, hand-feed kangaroos, marvel at the playful platypus, and enjoy a full daily schedule of keeper talks and activities, including Sheep Dog Show and Wild Lorikeet Feeding.
Bank Parklands is Brisbane's premier lifestyle and cultural destination. Located on the southern banks of the Brisbane River, its 17 hectares of lush parklands, world-class eateries, stunning river views and hundreds of delightful events all year round make it the perfect place to relax and unwind.
Mt Coot-Tha is a Brisbane icon forming a backdrop for the city and is Brisbane City Council's largest natural area, located just 15 minutes from the Brisbane CBD. The Mount Coot-Tha reserve contains more than 1600 hectares of open eucalypt forest, rainforest gullies, creek lines, waterfalls and spectacular views; offers a variety of walking tracks.

Important Dates

Abstract Submission: 14 May 21 May, 2023 (AoE)

Full Paper Submission: 21 May 28 May, 2023 (AoE)

Author Notification: 30 July, 2023

Camera-ready versions: 13 August 20 August, 2023

Journal First Submission Deadline: 1 September, 2023 (AoE)

Journal First Acceptance Notification: 2 October, 2023 (AoE)

Doctoral Symposium Submission Deadline: 25 August, 2023 (AoE)

Doctoral Symposium Acceptance Notification: 2 September, 2023 (AoE)

Doctoral Symposium Camera-ready Due: 5 9 September, 2023

Doctoral Symposium: 22 November, 2023

Conference Paper Submission and Publication

Submission should be done through the ICFEM 2023 submission page, handled by the EasyChair conference system.

As in previous years, the proceedings will be published in the Springer Lecture Notes in Computer Science series.

Papers should be written in English and should not exceed 16 pages (including references) in the Springer's LNCS format. Additional material may be placed in an appendix, to be read at the discretion of the reviewers and to be omitted in the final version. Formatting style files and further guidelines for formatting can be found at the Springer website (more details here).

Access submission portal

Journal-First Presentations

ICFEM 2023 is inviting journal-first presentations of papers published recently in the following journals:

  • ACM Transactions on Programming Languages and Systems
  • ACM Transactions on Software Engineering and Methodology
  • Formal Aspects of Computing
  • Formal Methods in System Design
  • IEEE Transactions on Software Engineering
  • Theoretical Computer Science

The presentations will offer the authors an opportunity to speak directly to their peers in the community, and also enrich the ICFEM program. The journal-first presentation will be listed in the conference program, yet the corresponding papers will not be part of the ICFEM proceedings as they have been published through the journals. At least one author of each accepted journal-first presentation must register for and attend the ICFEM conference to present the paper.

Evaluation and Selection

A journal-first presentation submitted to ICFEM must adhere to the following criteria:

  • The journal paper is in the scope of ICFEM 2023.
  • The paper was accepted by one of the participating journals no earlier than January 1, 2022.
  • The paper reports completely new research results or presents novel contributions that were not previously reported in prior work.
  • The paper does not extend prior work solely with additional proofs or algorithms, additional empirical results, or minor enhancements or variants of the results presented in the prior work.
  • The paper has not been presented at, and is not under consideration for, journal-first programs of other conferences.

Each submission will be evaluated according to these criteria. In case that the number of submissions is higher than expected, eligible submissions may be selected to be presented at the conference, and priority will be given to the papers that best fit the conference program.

How to Submit

Interested authors should submit a short presentation proposal consisting of the paper title, abstract, a short statement on how the work satisfies the above criteria, and the PDF of the original journal paper. Please submit a single PDF file and list all authors of the original journal paper as authors in EasyChair. No special formatting is required.

Submission Link

Doctoral Symposium Paper Submission

The ICFEM Doctoral Symposium is an international forum for PhD students studying all areas related to formal methods for software, hardware and system development. This forum is an excellent opportunity bringing together PhD students and well-known established researchers from the formal methods community. It will also provide PhD students with fruitful feedback and advice on their research approach and enable them to interact with other PhD students in order to stimulate the exchange of ideas and the sharing of experiences among participants. In summary, the PhD forum will provide PhD students with an ideal opportunity to present, share and discuss their research in a constructive and critical scientific atmosphere.

We seek submissions from PhD students who have either determined the direction of their thesis research (probably with some preliminary results already published), but who still have substantial work to complete; or PhD student participants who are in the early stages of their dissertations. It is not required to have a paper accepted at the main conference in order to participate in the ICFEM Doctoral Symposium.

Submissions to the Doctoral Symposium should include: Title of the research, the author name (single name) and affiliation; Context and motivation; Problem statement and related work; Proposed solutions and current research efforts, their significance, methodology, results and analysis, and future work. The paper should be prepared using the LNCS format and submitted in PDF format via EasyChair.

We accept two types of submissions: (a) 2-page extended abstracts which will not be included in the ICFEM proceedings; and (b) 6-page papers which will be published in the LNCS volume of Springer as part of the main ICFEM proceedings.

Authors with accepted submissions are expected to attend the Doctoral Symposium in person to present their work. A discounted registration fee for Doctoral Symposium participants will be announced later.

Submission Link

Official Sponsors

UQ     NUS     NTU     UNSW

Griffith     Monash     Concordia     Dependable Intelligence


ICFEM'23 is an outstanding opportunity for you to reach the "thought leaders" in this industry with your message, and for your Software Engineering team to network and exchange ideas with their peers in this unique and innovative forum.

Sponsors are offered the opportunity to reach over 100 software engineering experts, including researchers and industry practitioners such as developers, QA and engineering managers.

New sponsorship are welcome and any entity wishing to become an official sponsor may contact the sponsorship chair.

Conference Organising Committee

Steering Committee

David Basin, ETH Zurich, Switzerland
Michael Butler, University of Southampton, UK
Jin Song Dong, National University of Singapore, Singapore
Jifeng He, Shanghai Academy of AI Industrial Technology, China
Mike Hinchey, University of Limerick, Ireland
Shaoying Liu, Hiroshima University, Japan
Kazuhiro Ogata, JAIST, Japan
Shengchao Qin, Teesside University, UK (Chair)

General Co-Chairs

Jin Song Dong, National University of Singapore, Singapore
Guangdong Bai, The University of Queensland, Australia

Program Co-Chairs

Yi Li, Nanyang Technological University, Singapore
Sofiene Tahar, Concordia University, Canada

Finance Chair

Zhe Hou, Griffith University, Australia

Publicity Chair

Cheng-Hao Cai, Monash University at Suzhou, China
Neeraj Kumar Singh, IRIT-ENSEEIHT, Toulouse, France
Xiaodong Qi, Nanyang Technological University, Singapore

Journal First Co-Chairs

Mark Utting, The University of Queensland, Australia
Guowei Yang, The University of Queensland, Australia

Doctoral Symposium Chair

Yulei Sui, UNSW Sydney, Australia

Workshop Chair

Xiaofei Xie, Singapore Management University, Singapore

Sponsorship Chair

Kailong Wang, Huazhong University of Science and Technology, China

Local Co-Chairs

Naipeng Dong, The University of Queensland, Australia
Guowei Yang, The University of Queensland, Australia

Web Chair

Hao Guan, The University of Queensland, Australia

Program Committee

Yamine Ait Ameur, IRIT/INPT-ENSEEIHT, France
Behzad Akbarpour, NVIDIA, United States
Étienne André, Université de Lorraine, CNRS, Inria, LORIA, Nancy, France, France
Cyrille Valentin Artho, KTH Royal Institute of Technology, Sweden
Guangdong Bai, The University of Queensland, Australia
Christel Baier, TU Dresden, Germany
Richard Banach, University of Manchester, United Kingdom
Luís Soares Barbosa, University of Minho, Portugal
Hadrien Bride, Institute for Integrated and Intelligent Systems, Griffith University, Australia
Ana Cavalcanti, University of York, United Kingdom
Marsha Chechik, University of Toronto, Canada
Yuting Chen, Shanghai Jiao Tong University, China
Yean-Ru Chen, National Cheng Kung University, Taiwan
Yu-Fang Chen, Academia Sinica, Taiwan
Ranald Clouston, Australian National University, Australia
Florin Craciun, Babes-Bolyai University, Cluj, Romania
Ana De Melo, University of São Paulo, Brazil
Thi Thu Ha Doan, Freiburg University, Germany
Naipeng Dong, National University of Singapore, Singapore
Aaron Dutle, NASA Langley Research Center, United States
Yasmeen Elderhalli, Synopsys, Canada
Santiago Escobar, Universitat Politècnica de València, Spain
Flavio Ferrarotti, Software Competence Centre Hagenberg, Austria
Marc Frappier, Université de Sherbrooke, Canada
Lindsay Groves, Victoria University of Wellington, New Zealand
Osman Hassan, National University of Sciences & Technology, Pakistan
Xudong He, Florida International University, United States
Zhe Hou, Griffith University, Australia
Fuyuki Ishikawa, National Institute of Informatics, Japan
Eun-Young Kang, University of Southern Denmark, Denmark
Tsutomu Kobayashi, Japan Aerospace Exploration Agency, Japan
Mark Lawford, McMaster University, Canada
Jiaying Li, Microsoft, China
Shang-Wei Lin, Nanyang Technological University, Singapore
Guanjun Liu, Tongji University, China
Zhiming Liu, Southwest University, China
Si Liu, ETH Zurich, Swizerland
Brendan Mahony, DSTO, Australia
Frederic Mallet, Universite Nice Sophia-Antipolis, France
Panagiotis Manolios, Northeastern University, United States
Heiko Mantel, TU Darmstadt, Germany
Narciso Martí-Oliet, Universidad Complutense de Madrid, Spain
Dominique Mery, Université de Lorraine, LORIA, France
Stephan Merz, Inria Nancy, France
Stefan Mitsch, Carnegie Mellon University, United States
Magnus Myreen, Chalmers University, Sweden
Shin Nakajima, National Institute of Informatics, Japan
Masaki Nakamura, Toyama Prefectural University, Japan
Michael Norrish, Australian National University, Australia
Jun Pang, University of Luxembourg, Luxembourg
Yu Pei, The Hong Kong Polytechnic University, Hong Kong
Shengchao Qin, Teesside University, United Kingdom
Silvio Ranise, University of Trento and Fondazione Bruno Kessler, Trento, Italy, Italy
Elvinia Riccobene, Computer Science Dept., University of Milan, Italy
Adrian Riesco, Universidad Complutense de Madrid, Spain
Subhajit Roy, Indian Institute of Technology Kanpur, India
Rubén Rubio, Universidad Complutense de Madrid, Spain
David Sanan, Singapore Institute of Technology, Singapore
Valdivino Santiago, Instituto Nacional de Pesquisas Espaciais, Brazil
Meng Sun, Peking University, China
Jing Sun, The University of Auckland, New Zealand
Elena Troubitsyna, KTH, Sweden
Ionut Tutu, Simion Stoilow Institute of Mathematics of the Romanian Academy, Romania
Bow-Yaw Wang, Academia Sinica, Taiwan
Hai H. Wang, University of Aston, United Kingdom
Naijun Zhan, Institute of Software, Chinese Academy of Sciences, China
Min Zhang, East China Normal University, China
Yongwang Zhao, Zhejiang University, China
Peter Ölveczky, University of Oslo, Norway

Doctoral Symposium Program Committee

Xiaoyu Sun, Australian National University, Australia
Yuekang Li, UNSW Sydney, Australia
Xiaoyi Zhang, University of Science and Technology Beijing, China
Ruitao Feng, Singapore Management University, Singapore
Dipankar Chaki , UNSW Sydney, Australia
Hsu Myat Win , RMIT University, Australia

Local Support Team

Baiqi Chen, The University of Queensland, Australia
Shuofeng Liu, The University of Queensland, Australia