The 25th International Conference on Formal Engineering Methods

2 ~ 6 December 2024 - Hiroshima, Japan

Welcome to the website of the 25th International Conference on Formal Engineering Methods (ICFEM 2024)

Since it was started in Hiroshima, Japan in 1997, ICFEM has provided a forum for both researchers and practitioners to discuss and exchange their experience and results in research on theories, methods, languages, and supporting tools for integrating formal methods into conventional software engineering technologies to provide more effective and efficient approaches to large-scale software engineering. The goal of this conference is to bring together industrial, academic, and government experts in both formal methods and software engineering to help advance the state of the art.

At its first return to Hiroshima since 1997, ICFEM 2024 will celebrate the 25th anniversary of the ICFEM conference series. Researchers, practitioners, tool developers, and users are all welcome to submit papers and participate in the conference. We look forward to your contributions and participation.

Scope and Topics

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

  • Formal specification and modeling
  • Formal approaches to fault prevention and detection
  • Abstraction, refinement, and evolution
  • Formal verification and validation
  • Integration of formal methods and testing
  • Integration of formal methods and review
  • SAT/SMT solvers for software analysis and testing
  • Practical formal methods
  • Applications of formal methods
  • Formal approaches to software maintenance
  • Formal approaches to safety-critical system development
  • Supporting tools for formal methods
  • Formal methods for agile development
  • Formal methods for human-machine pair programming
  • Formal methods for AI Systems
  • Formal methods for Cyber-physical systems and IoT
  • Formal certification of products
  • Industrial case studies



Venue and Accommodation

The 25th International Conference on Formal Engineering Methods (ICFEM 2024) will take place in International Conference Center Hiroshima.

The International Conference Center Hiroshima (ICCH) is located within Peace Memorial Park with the purpose of promoting international exchange and improving civic culture. Equipped with a large hall that can accommodate up to 1,504 people, an international conference hall, and large, medium and small conference rooms, the venue is ideal for concerts, lectures, domestic and international conferences, as well as exhibitions and corporate and organizational meetings. It is widely used for various purposes.


Hiroshima, a symbol of resistance and rebirth, deserves to be at the top of your bucket list of places to visit in Japan. The City of Peace, which just welcomed the latest G7 Summit, is a must-see destination in Japan's south. With a rich historic past that extends well beyond the tragic 1945 events, a vibrant city life, wonderful local cuisine, and gorgeous surroundings as it lies by the blue waters of Hiroshima Bay, let’s take a look at everything Hiroshima has to offer! (more details here).



Keynote Speakers

Mike Hinchey is Professor of Software Engineering at University of Limerick, Ireland, where he was previously Head of Department of Computer Science and Information Systems and Director of Lero-the Science Foundation Ireland Research Centre for Software, a national research centre headquartered at University of Limerick. He is Past President of IFIP, the International Federation for Information Processing ( and Past Chair of the IEEE UK & Ireland Section. He is Director-elect of IEEE Region 8 (Europe, Middle East, Africa) and serves on IEEE Computer Society Board of Governors. Prior to joining University of Limerick, Professor Hinchey was the Director of the NASA Software Engineering Laboratory. In 2009, he was awarded NASA’s Kerley Award as Innovator of the Year and is one of only 36 people recognized in the NASA Inventors Hall of Fame. Professor Hinchey holds a B.Sc. in Computer Systems from University of Limerick, an M.Sc. in Computation (Mathematics) from University of Oxford and a PhD in Computer Science from University of Cambridge. Professor Hinchey is a Chartered Engineer, Chartered Engineering Professional, Chartered Mathematician and Chartered Information Technology Professional, as well as a Fellow of the IET, British Computer Society, Engineers Ireland, and Irish Computer Society, of which he is also Past President. He is Editor-in-Chief of Innovations in Systems and Software Engineering: a NASA Journal and Journal of the Brazilian Computer Society. In 2018, he became an Honorary Fellow of the Computer Society of India and was the SEARCC Global ICT Professional of the Year 2018.

Title: Formal Specification of Autonomy Features with ARE and KnowLang


Autonomous systems, such as autonomous vehicles, extend upstream the regular software-intensive systems with special autonomy features. The identification of such features is not necessarily an easy task. Sometimes, those can be explicitly stated by stakeholders or in preliminary material available to requirements engineers. Often though, they are implicit, so a process of formal specification intended to capture the autonomy features has to be undertaken. This paper elaborates on a methodology for capturing and specification of autonomy features where autonomy requirements are captured with ARE (Autonomy Requirements Engineering) and then are specified with KnowLang. a framework for knowledge representation and reasoning. In this approach, autonomy features are detected as special self-* objectives backed up by different capabilities and quality characteristics. The self-* objectives provide the system’s ability to autonomously discover, diagnose, and cope with various problems. The captured autonomy requirements are formally specified with the KnowLang notation and then compiled to a knowledge base that is to be used by the KnowLang Reasoner.

Naijun Zhan is a distinguished research professor of Institute of Software Chinese Academy of Sciences (ISCAS). He got his bachelor degree and master degree both from Nanjing University, and his PhD from ISCAS. Prior to join ISCAS, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research fellow. His research interests cover formal design of real-time, embedded and hybrid systems, program verification, modal and temporal logic, and so on. He is in the editorial boards of Journal of Automated Reasoning, Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, Journal of Electronics, and Journal of Computer Research and Development, a member of the steering committees of SETTA and MEMOCODE, the pc co-chairs of FM 2021, SETTA 2016, the general co-chairs of MEMOCODE 2018, MEMOCODE2019 and ICESS 2019, and serves more than 100 international conferences program committees e.g., CAV, FM, TACAS, RTSS, HSCC, ICCPS, EMSOFT and so on. He published more than 100 papers in international leading journals and conferences, 2 books and 4 book chapters, and edited 4 conference proceedings and 4 journal special issues.

Title: Synthesizing (Differential) Invariants by Reduction Non-Convex Programming to SDP


Invariant Generation plays a central role in the verification of programs and hybrid systems. As the constraint solving techniques advance rapidly in recent years, particularly optimization-based constraint solving, optimization based invariant generation becomes more and more promising and has been successfully applied to verification of programs and hybrid systems. However, how to deal with non-convex programming derived from invariant generation is still challenging. In this talk, I report our recent work on efficient invariant generation by reduction non-convex programming to SDP.

Mark Lawford is Chair and Professor of the Department of Computing and Software at McMaster University (Canada). He is a Co-Founder and a past Director of McMaster Centre for Software Certification (McSCert), the 2024 IEEE TCSE Synergy award recipient. He joined McMaster University in 1998, where he helped to develop the software engineering and mechatronics engineering programs. Throughout his career he has work with industry on the practical application of formal methods and model based software engineering to safety critical real-time software. After working with industry partners in the nuclear and medical domains earlier in his career, over the past decade he has increasingly focused on working with OEMs on assurance of automotive systems.

Title: Challenges and Opportunities in Assurance of Software Defined Vehicle


Automotive innovation is increasingly software driven. As a result of the competitive environment requiring a yearly release of new automotive models featuring the latest driver assistance features and innovation in electrification, safety critical software is being developed at an unprecedented scale on extremely tight deadlines. To be competitive automotive manufacturers and parts suppliers need to change how they develop and assure software intensive systems. This presents a tremendous opportunity for researchers in the application of formal methods and model based software engineering to have a significant impact on industry practice. In this talk we highlight our recent work on model based software engineering, incremental assurance and the potential for applications of formal methods to help the automotive industry make the transition to the Software Defined vehicle.

Important Dates

Full Paper Submissions: 8 July, 2024 (strict)

Acceptance / Rejection Notification: 9 September, 2024

Camera-ready Papers: 27 September, 2024

Workshop/Tutorial Proposals: 5 July, 2024

Conference Paper Submission and Publication

Submission should be done through the ICFEM 2024 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.

Submissions to the conference must not have been published or be concurrently considered for publication elsewhere. Papers should be written in English. Regular papers should not exceed 18 pages (20 pages including references and appendix) and short papers should not exceed 12 pages (including references and appendix) in Springer LNCS format. In addition to paper submissions, we will also organize several tracks, including Doctoral Symposium, Industrial Applications, and Journal-First Presentations. The accepted submissions for both Doctoral Symposium and Industrial Applications Tracks will be included in the proceedings of ICFEM 2024. Formatting style files and further guidelines for formatting can be found at the Springer website (more details here).

Journal-First Presentations

ICFEM 2024 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.

How to Submit

Interested authors should submit a short presentation proposal consisting of the paper title, abstract, a short statement how the work is related to the scope of the ICFEM 2024, 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 format is required.

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.

The submission should not exceed 6-pages in LNCS format and accepted submissions will be included in the ICFEM 2024 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.

Industrial Applications

Submissions to the Industrial Applications track should clearly describe how the relevant formal methods are applied to the development or maintenance of specific software or hardware systems in an engineering manner and should not exceed 6-pages in the LNCS format. Accepted submissions will be included in the proceedings of ICFEM 2024.




HU     IPJ

Supported by Hiroshima University

Information Processing Society of Japan

Conference Organizing 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, Xidian University, China(Chair)

General Chair

Shaoying Liu, Hiroshima University, Japan

Program Chairs

Kazuhiro Ogata, JAIST, Japan
Meng Sun, Peking University, China
Dominique Méry, LORIA, Telecom Nancy, University of Lorraine, France

Financial Chair

Fumiko Nagoya, Nihon University, Japan

Publicity Chair

Yuting Chen, Shanghai Jiao Tong University, China
Yamine Ait-Ameur, IRIT-ENSEEIHT, Toulouse, France

Track-Organizing Chair

Weikai Miao, ECNU, China

Workshop/Tutorial Chair

Wuwei Shen, Western Michigan University, USA

Web Chair

Yuxiang Shang, Hiroshima University, Japan

Local Arrangement Chairs

Naoko Wakiya, Hiroshima Shudo University, Japan
Yanzhao Xia, Hiroshima University, Japan

Leadership Appreciation Chair

Shengchao Qin, Xidian University, China

Program Committee

Yamine Ait Ameur, IRIT/INPT-ENSEEIHT, France
Étienne André, Université de Lorraine, France
Cyrille Valentin Artho, KTH Royal Institute of Technology, Sweden
Guangdong Bai, The University of Queensland, Australia
Christel Baier, TU Dresden, Germany
Lei Bu, Nanjing University, China
Ana Cavalcanti, University of York, United Kingdom
Yean-Ru Chen, National Cheng Kung University, Taiwan
Yuting Chen, Shanghai Jiao Tong University, China
Zhenbang Chen, NUDT, China
Ranald Clouston, Australian National University, Australia
Florin Craciun, Babes-Bolyai University, Romania
Ana De Melo, University of São Paulo, Brazil
Canh Minh Do, JAIST, Japan
Thi Thu Ha Doan, Freiburg University, Germany
Naipeng Dong, National University of Singapore, Singapore
Aaron Dutle, NASA Langley Research Center, United States
Santiago Escobar, Universitat Politècnica de València, Spain
Flavio Ferrarotti, Software Competence Centre Hagenberg, Austria
Marc Frappier, Université de Sherbrooke, Canada
Daniel Gaina, Kyushu University, Japana
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
Mark Lawford, McMaster University, Canada
Jiaying Li, Microsoft, China
Shang-Wei Lin, Nanyang Technological University, Singapore
Guanjun Liu, Tongji University, China
Si Liu, ETH Zurich, Swizerland
Zhiming Liu, Southwest University, China
Frederic Mallet, Universite Nice Sophia-Antipolis, France
Heiko Mantel, TU Darmstadt, Germany
Diego Marmsoler, University of Exeter, United Kingdom
Narciso Martí-Oliet, Universidad Complutense de Madrid, Spain
Stephan Merz, Inria Nancy, France
Rosemary Monahan, Maynooth University, Ireland
Shin Nakajima, National Institute of Informatics, Japan
Masaki Nakamura, Toyama Prefectural University, Japan
Peter Ölveczky, University of Oslo, Norway
Jun Pang, University of Luxembourg, Luxembourg
Yu Pei, The Hong Kong Polytechnic University, Hong Kong
Shengchao Qin, Xidian University, China
Silvio Ranise, University of Trento and Fondazione Bruno Kessler, Italy
Elvinia Riccobene, University of Milan, Italy
Adrian Riesco, Universidad Complutense de Madrid, Spain
Markus Roggenbach, Swansee University, UK
Subhajit Roy, Indian Institute of Technology Kanpur, India
Rubén Rubio, Universidad Complutense de Madrid, Spain
David Sanan, Singapore Institute of Technology, Singapore
Jing Sun, The University of Auckland, New Zealand
Sofiene Tahar, Concordia University, Canada
Maurice ter Beek, ISTI CNR PISA, Italy
Cong Tian, Xidian University, China
Duong Dinh Tran, JAIST, Japan
Elena Troubitsyna, KTH, Sweden
Tatsuhiro Tsuchiya, Osaka University, Japan
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
Tomoyuki Yokogawa, Okayama Prefectural University, Japan
Min Zhang, East China Normal University, China
Xiyue Zhang, University of Oxford, United Kingdom
Yongwang Zhao, Zhejiang University, China