- FMIndia - mail.cmi.ac.in

VSTTE 2025 (co-located with FMCAD 2025): Call for papers
by Supratik Chakraborty 18 Jun '25

18 Jun '25

VSTTE 2025 17th International Conference on Verified Software: Theories, Tools, and Experiments October 06-07, 2025, Menlo Park, California, USA Co-located with Formal Methods in Computer-Aided Design 2025 (_FMCAD 2025 <https://fmcad.org/FMCAD25/>_) Key Information Conference Website: _https://systemf.epfl.ch/etc/vstte2025/ <https://systemf.epfl.ch/etc/vstte2025/>_ Paper submission Deadline: July 18th AoE This year, VSTTE accepts both (short and long) regular papers to be included in post-conference proceedings and work-in-progress (presentation only) papers. Overview The goal of the VSTTE conference series is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation. The Verified Software Initiative (VSI), spearheaded by Tony Hoare and Jayadev Misra, is an ambitious research program for making large-scale verified software a practical reality. The International Conference on Verified Software: Theories, Tools and Experiments (VSTTE) is the main forum for advancing the initiative. VSTTE brings together experts spanning the spectrum of software verification in order to foster international collaboration on the critical research challenges. The theoretical work includes semantic foundations and logics for specification and verification, and verification algorithms and methodologies. The tools cover specification and annotation languages, program analyzers, model checkers, interactive verifiers and proof checkers, automated theorem provers and SAT/SMT solvers, and integrated verification environments. The experimental work drives the research agenda for theory and tools by taking on significant specification/verification exercises covering hardware, operating systems, compilers, computer security, parallel computing, and cyber-physical systems. Call for papers and work-in-progress presentations VSTTE 2025 welcomes submissions describing significant advances in the production of verified software, i.e. software that has been proved to meet its functional specifications. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains. We are especially interested in submissions describing large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. We also welcome papers describing novel experiments and case studies evaluating verification techniques and technologies. In addition to regular papers, we welcome submissions on in-progress verified software projects to a “work-in-progress (presentation-only)” track. Work-in-progress contributions will not appear in the post-proceedings of the conference. Submissions describing work of interest to the software verification community, but that could not be accepted for publication in the conference proceedings, may be invited to the “work-in-progress (presentation-only)” track, on a case-by-case basis. Topics of interest for this conference include, but are not limited to, requirements modeling, specification languages, specification/verification/certification case studies, formal calculi, software design methods, automatic code generation, refinement methodologies, compositional analysis, verification tools (e.g., static analysis, dynamic analysis, model checking, theorem proving, satisfiability), tool integration, benchmarks, challenge problems, and integrated verification environments. Submissions VSTTE 2025 accepts both long (limited to 16 pages, excluding references) and short (limited to 10 pages, excluding references) paper submissions. Short submissions also cover “verification pearls” describing an elegant proof or proof technique. Submitted research papers and system descriptions must be original and not submitted for publication elsewhere. Papers may be submitted via EasyChair at the _VSTTE 2025 conference submission page <https://easychair.org/conferences/?conf=vstte25>_. The use of LaTeX and the _Springer LNCS class files <https://www.springer.com/gp/computer-science/lncs/conference-proceedings-gu…>_ is strongly encouraged. Submissions that are not in the proper format or are too long will not be considered. Accepted regular-track papers will be included in the post-conference proceedings of VSTTE 2025, which will be published as a LNCS volume by Springer-Verlag. Authors of those papers will have to transfer copyright of their contribution to Springer-Verlag. Important Dates * Abstract submission: July 14th AoE * Paper submission: July 18th AoE * Notification of acceptance: Aug 31th (AoE) * Final pre-conference paper submission: September 26th (AoE) * Conference: October 6th-7th * Camera-ready for papers included in post-conference proceedings: TBA Invited speakers * _Caroline Trippel <https://cs.stanford.edu/people/trippel/>_ (Stanford University) * _Grant Passmore <https://www.imandra.ai/about>_ (Imandra) Invited tutorial speakers * _Pierre-Yves Strub <https://www.strub.nu/>_ (PQShield) Chairs Steering Committee * _Supratik Chakraborty <https://www.cse.iitb.ac.in/~supratik/>_ (IIT Bombay, India) * _Natarajan Shankar <https://www.csl.sri.com/~shankar/>_ (SRI International) Program Chairs * _Clément Pit-Claudel <https://pit-claudel.fr/clement/>_ (EPFL) * _Katherine Kosaian <https://sites.google.com/view/katherinekosaian>_ (University of Iowa)

1 0

DataMod 2025 - First Call for Papers
by Ouadie Khebbeb 18 Jun '25

18 Jun '25

DataMod 2025 - 13th International Symposium "From Data to Models and Back" Toledo, Spain, 10-11 November 2025 Website: https://datamod-symposium.github.io/DataMod-2025/ DataMod 2025 is a satellite event of the 23rd International Conference of Software Engineering and Formal Methods (SEFM 2025): https://sefm-conference.github.io/2025/ -------------------------------------------------------------------------------- Abstract submission deadline (optional): 22 August 2025 Paper submission deadline: 29 August 2025 -------------------------------------------------------------------------------- CONTEXT & OBJECTIVES DataMod 2025 aims at bringing together practitioners and researchers from academia, industry and research institutions interested in the combined computational modelling methods with data-driven techniques from the areas of knowledge management, data mining and machine learning. Modelling methodologies of interest include automata, agents, Petri nets, process algebras and rewriting systems. Application domains include social systems, ecology, biology, medicine, smart cities, governance, security, education, software engineering, and any other field that deals with complex systems and large amounts of data. Papers can present research results in any of the themes of interest for the symposium, as well as application experiences, tools and promising preliminary ideas. Papers dealing with synergistic approaches that integrate modelling and knowledge management/discovery, or that exploit knowledge management/discovery to develop/synthesise system models are especially welcome. Authors are invited to submit original research or tool papers on any relevant topic. These can either be normal or short papers. Short papers can discuss new ideas which are at an early stage of development and which have not yet been thoroughly evaluated. TOPICS Modelling and analysis methodologies include: - Agent-based Methodologies - Automata-based Notations - Big Data Analytics - Cellular Automata - Classification - Clustering, Segmentation and Profiling - Conformance Analysis - Constraint Programming - Data Mining - Differential Equations - Game Theory - Machine Learning - Membrane Systems - Network Theory and Analysis - Ontologies - Optimisation Modelling - Petri Nets - Process Calculi - Process Mining - Rewriting Systems - Spatio-temporal Data Analysis/Mining - Statistical Model Checking - Text Mining - Topological Data Analysis Application domains include: - Biology - Brain Data and Simulation - Business Process Management - Climate Change - Cybersecurity - Ecology - Education - Environmental Risk Assessment and Management - Enterprise Architectures - Epidemiology - Genetics and Genomics - Governance - HCI and Human Behaviour - Open Source Software Development and Communities - Pharmacology - Resilience Engineering - Safety and Security Risk Assessment - Social Good - Social Software Engineering - Social Systems - Sustainable Development - Threat Modelling and Analysis - Urban Ecology - Smart Cities and Smart Lands Synergistic approaches include: (1) Use of modelling methods and notations in a knowledge management/discovery context (2) Development and use of common modelling and knowledge management/discovery frameworks to explore and understand complex systems from the application domains of interest SUBMISSION AND PUBLICATION All contributions in the form of either - regular (research, tool or position) paper, up to 16 pages (excluding references) - short (research, tool or position) paper, up to 8 pages (excluding references) will be reviewed by three members of the Program Committee. Authors are invited to submit their contributions via Easychair https://easychair.org/conferences/?conf=datamod2025 In addition, presentation reports will be considered having the following form: - presentation report, up to 4 pages Presentation reports concern recent or ongoing work on relevant topics and ideas, for timely discussion and feedback at the workshop. There is no restriction as to previous/future publication of the contents of a presentation. Typically, a presentation is based on a paper which recently appeared (or which is going to appear) in the proceedings of another recognised conference, or which has not yet been submitted. Presentation reports will receive a lightweight review to establish their relevance for DataMod. Authors are invited to submit their presentation report via Easychair https://easychair.org/conferences/?conf=datamod2025 All papers should be written in English and formatted according to the LNCS style. Paper formatting guidelines according to LNCS style are available here: http://www.springer.com/lncs Detailed information on the submission procedure and format are available on the symposium web page: https://datamod2025.github.io/ Accepted papers (both regular and short) will be included in a dedicated LNCS post-proceedings volume published by Springer after the Symposium. Condition for inclusion in the proceedings is that at least one of the co-authors attends and presents the paper at the Symposium. IMPORTANT DATES Abstract Submission deadline (optional): 22 August 2025 Paper Submission deadline: 29 August 2025 Notification: 30 September 2025 Revised Version: 7 October 2025 Symposium: 10-11 November 2025 KEYNOTE SPEAKERS * TBA PROGRAM CO-CHAIRS * Livia Lestingi, Politecnico di Milano, Italy * Gwen Salaün, Université Grenoble Alpes, France PROGRAM COMMITTEE * Oana Andrei, University of Glasgow * Kyungmin Bae, Pohang University of Science and Technology (POSTECH) * Juliana Bowles, School of Computer Science, University of St Andrews * Giovanna Broccia, ISTI-CNR, FMT Lab * Antonio Cerone, Nazarbayev University * Robert Clarisó, Universitat Oberta de Catalunya * Carla Ferreira, Universidade NOVA de Lisboa * Marc Frappier, Université de Sherbrooke * Elisa Gonzalez Boix, Vrije Universiteit Brussel * Riccardo Guidotti, University of Pisa * Alexander Kocian, University of Pisa * Ricardo M. Czekster, Aston University * José Machado, University of Minho, DI, ALGORITMI/LASI * Paolo Milazzo, Dipartimento di Informatica - Università di Pisa * Pedro Ribeiro, University of York * Arpit Sharma, Indian Institute of Science Education and Research * Volker Stolz, Høgskulen på Vestlandet * Martin Tappler, TU Wien * Thais Webber, Aston University * Lina Ye, CentraleSupélec, LMF, University Paris-Saclay, France CONTACT > All inquiries should be sent to datamod2025(a)easychair.org

1 0

IARCS Verification Seminar Series -- Talk by Shahaf Bassan on June 12 at 1900 hrs IST
by VSS IARCS 12 Jun '25

12 Jun '25

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Shahaf Bassan, a senior PhD student in the Katz Lab at the Hebrew University of Jerusalem specializing in explainable AI. The talk is scheduled on Thursday, June 12, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NTRxaDRxdG…> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/) and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: “Formal XAI”: Can we formally explain ML models? Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: The goal of explainability is to make sense of the decisions made by black-box ML models. Unfortunately, many existing explanation methods are heuristic, which makes them unreliable. In this talk, I will present our work on developing techniques that provide explanations with formal guarantees, ensuring their trustworthiness. These techniques often rely on formal verification, particularly neural network verification tools. In addition, we examine these explanations from a theoretical perspective - studying the computational challenges they pose and exploring ways to build practical tools that address these challenges and enable the generation of reliable explanations for ML models. Bio: Shahaf Bassan is a senior PhD student in the Katz Lab at the Hebrew University of Jerusalem specializing in explainable AI. His research focuses on developing explanation techniques with formally provable guarantees, at the intersection of explainability, formal verification, and ML theory. His work spans both theoretical foundations and practical applications. Sahaf has presented his research at leading conferences in formal verification (e.g., TACAS) and machine learning (e.g., ICML, ICLR). His research goal is to enhance trust in ML models by providing trustworthy, verifiable explanations.

1 0

IARCS Verification Seminar Series -- Talk by Shahaf Bassan postponed to June 12, 1900 hrs IST
by VSS IARCS 09 Jun '25

09 Jun '25

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Shahaf Bassan, a senior PhD student in the Katz Lab at the Hebrew University of Jerusalem specializing in explainable AI. The talk is scheduled on Thursday, June 12, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NTRxaDRxdG…> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/) and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: “Formal XAI”: Can we formally explain ML models? Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: The goal of explainability is to make sense of the decisions made by black-box ML models. Unfortunately, many existing explanation methods are heuristic, which makes them unreliable. In this talk, I will present our work on developing techniques that provide explanations with formal guarantees, ensuring their trustworthiness. These techniques often rely on formal verification, particularly neural network verification tools. In addition, we examine these explanations from a theoretical perspective - studying the computational challenges they pose and exploring ways to build practical tools that address these challenges and enable the generation of reliable explanations for ML models. Bio: Shahaf Bassan is a senior PhD student in the Katz Lab at the Hebrew University of Jerusalem specializing in explainable AI. His research focuses on developing explanation techniques with formally provable guarantees, at the intersection of explainability, formal verification, and ML theory. His work spans both theoretical foundations and practical applications. Sahaf has presented his research at leading conferences in formal verification (e.g., TACAS) and machine learning (e.g., ICML, ICLR). His research goal is to enhance trust in ML models by providing trustworthy, verifiable explanations.

1 0

DPM 2025 - CFP - Data Privacy Manamgement, co-located with ESORICS 2025
by Guillermo Navarro-Arribas 06 Jun '25

06 Jun '25

(Apologies for cross-posting) CALL FOR PAPERS ****************************************************** Data Privacy Management (DPM 2025) 20th International Workshop September 25, 2025, Toulouse, France (co-located with ESORICS 2025) website: https://deic.uab.cat/dpm/dpm2025/ ****************************************************** IMPORTANT DATES ====================== Submission Deadline: -- June 17, 2025 Notification: -- July 31, 2025 Camera Ready: -- September 5, 2025 ====== SCOPE ====== DPM is an annual international workshop covering research in data privacy management. Organizations are increasingly concerned about the privacy of information that they manage (as witnessed, for example, by lawsuits filed against organizations for violating the privacy of customer's data). Thus, the management of privacy-sensitive information is very critical and important for every organization. This poses several challenging problems, such as how to translate the high-level business goals into system-level privacy policies, administration of privacy-sensitive data, privacy preserving data integration and engineering, privacy preserving access control mechanisms, information-oriented security, and query execution on privacy-sensitive data for partial answers. Starting from these observations, the aim of DPM is to discuss and exchange ideas related to data privacy management. We invite papers from researchers and practitioners working in privacy, security, trustworthy data systems and related areas to submit their original papers in this workshop. Submissions by PhD students as well as controversial ideas are encouraged. Case studies (successful or not) are also encouraged. TOPICS ======== Topics of interest include, but are not limited to: - Privacy in Machine Learning - Privacy Information Management - Privacy Policy-based Infrastructures and Architectures - Privacy-oriented Access Control Languages and Models - Privacy in Trust Management - Privacy in Cryptocurrencies - Privacy Data Integration - Privacy Risk Assessment and Assurance - Privacy Services - Privacy Policy Analysis - Data Protection Regulations in Practice - Cryptographic Protocols for Privacy - Query Execution over Privacy Sensitive Data - Privacy Preserving Data Mining - Privacy for Integrity-based Computing - Privacy Monitoring and Auditing - Privacy in Social Networks - Privacy in Ambient Intelligence (AmI) Applications - Individual Privacy vs. Corporate/National Security - Privacy in computer networks - Privacy and RFIDs - Privacy and Big Data - Privacy in sensor networks - Privacy in the Internet of Things PAPER SUBMISSIONS =================== Submitted papers must not substantially overlap papers that have been published or that are simultaneously submitted to a journal or a conference with proceedings. Papers can be submitted as Full Papers or Short Papers. Full papers should be at most 16 pages in the LNCS format, including the bibliography and well-marked appendices. Short papers should be at most 8 pages in the LNCS format, including the bibliography and well-marked appendices. Program Committee members are not required to read the appendices, so papers should be intelligible without them. Authors should indicate whether their paper is a short paper to differentiate them from full papers. All submissions must be written in English. It is planned to have accepted papers published by Springer in the Lecture Notes in Computer Science (LNCS) series, the LNCS template can be found at: http://www.springer.com/computer/lncs/lncs+authors. Submission should be done through the ESORICS 2025 Easychair: https://easychair.org/conferences/?conf=esorics2025 and the select the track: DPM Workshop. Only PDF files will be accepted (a Latex source file will be required for the final version of the accepted papers). All papers will be refereed. Accepted papers must be presented at the Workshop. At least one author of each accepted paper must register to the workshop, by the early date indicated by the organizers, and present the paper. PROGRAM CHAIRS =============== Joaquin Garcia-Alfaro (Institut Polytechnique de Paris) Guillermo Navarro-Arribas (Universitat Autonoma de Barcelona) PROGRAM COMMITTEE ================= - Abderrahim Ait Wakrime (Mohammed V University) - Ken Barker (University of Calgary) - Elisa Bertino (Purdue University) - Alessandro Brighente (University of Padova) - Jordi Casas-Roma (Universitat Autonoma de Barcelona) - Jordi Castella-Roca (Universitat Rovira i Virgili) - Depeng Chen (Anhui University) - Mathieu Cunche (University of Lyon / Inria) - Frederic Cuppens (Polytechnique Montreal) - Sabrina De Capitani di Vimercati (Universita degli Studi di Milano) - Jose M. De Fuentes (Universidad Carlos III de Madrid) - Josep Domingo-Ferrer (Universitat Rovira i Virgili) - Lorena Gonzalez Manzano (Universidad Carlos III de Madrid) - M. Emre Gursoy (Koç University) - Guy-Vincent Jourdan (University of Ottawa) - Florian Kammueller (Middlesex University London) - Bruce Kapron (University of Victoria) - Sokratis Katsikas (Norwegian University of Science and Technology) - Christophe Kiennert (Telecom SudParis) - Hiroaki Kikuchi (Meiji University) - Evangelos Kranakis (Carleton University) - Romain Laborde (Universite de Toulouse) - Patrick Lacharme (Ensicaen) - Giovanni Livraga (University of Milan) - Brad Malin (Vanderbilt University) - Lukas Malina (Brno University of Technology) - Zoltan Mann (University of Halle-Wittenberg) - David Megias (Universitat Oberta de Catalunya) - Gerardo Pelosi (Politecnico di Milano) - Cristina Perez-Sola (Universitat Autonoma de Barcelona) - Ruben Rios (University of Malaga) - Pierangela Samarati (Universita degli Studi di Milano) - Vicenc Torra (Umea University) - Alexandre Viejo (Universitat Rovira i Virgili) - Isabel Wagner (University of Basel) - Jens Weber (University of Victoria) - Nicola Zannone (Eindhoven University of Technology)

1 0

IARCS Verification Seminar Series -- Talk by Shahaf Bassan on June 10 at 1900 hrs IST
by VSS IARCS 01 Jun '25

01 Jun '25

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Shahaf Bassan, a senior PhD student in the Katz Lab at the Hebrew University of Jerusalem specializing in explainable AI. The talk is scheduled on Tuesday, June 10, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NTRxaDRxdG…> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/) and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: “Formal XAI”: Can we formally explain ML models? Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: The goal of explainability is to make sense of the decisions made by black-box ML models. Unfortunately, many existing explanation methods are heuristic, which makes them unreliable. In this talk, I will present our work on developing techniques that provide explanations with formal guarantees, ensuring their trustworthiness. These techniques often rely on formal verification, particularly neural network verification tools. In addition, we examine these explanations from a theoretical perspective - studying the computational challenges they pose and exploring ways to build practical tools that address these challenges and enable the generation of reliable explanations for ML models. Bio: Shahaf Bassan is a senior PhD student in the Katz Lab at the Hebrew University of Jerusalem specializing in explainable AI. His research focuses on developing explanation techniques with formally provable guarantees, at the intersection of explainability, formal verification, and ML theory. His work spans both theoretical foundations and practical applications. Sahaf has presented his research at leading conferences in formal verification (e.g., TACAS) and machine learning (e.g., ICML, ICLR). His research goal is to enhance trust in ML models by providing trustworthy, verifiable explanations.

1 0

ICFEM 2025 (Hangzhou): Extended deadline
by Étienne André 27 May '25

27 May '25

============================================================ Call for papers ICFEM 2025 The 26th International Conference on Formal Engineering Methods 10-13 November 2025 (Hangzhou, China) ============================================================ https://icfem2025.github.io ** NEW: EXTENDED DEADLINES** - Abstract Submission Deadline: May 25, 2025 => 11th June 2025 - Full Paper Submission Deadline: June 1, 2025 => 15th June 2025 ** NEW: SPECIAL ISSUES** - Invited extended versions of selected papers will be recommended to a special issue of Formal Aspects of Computing after the conference proceedings. - After the conference, the best software linked to a paper (typically any paper with a dedicated implementation) will be recommended to a special issue of the Software track of Elsevier's Science of Computer Programming journal. *ABOUT ICFEM* ICFEM is an internationally leading conference series in formal methods and software engineering. Since 1997, ICFEM has served 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, as well as in theoretical work that promises to bring practical and tangible benefits. ICFEM has been hosted in many countries around the world. This year, the 26th International Conference on Formal Engineering Methods will be held in Hangzhou, China (birthplace of DeepSeek). ICFEM 2025 welcomes submissions from researchers and practitioners worldwide to advance the field of formal methods and software engineering. *KEYNOTE SPEAKERS* - Jifeng He, Tongji University, China - Mariëlle Stoelinga, Radboud University & University of Twente, the Netherland - Jim Woodcock, University of York, UK - Yongwang Zhao, Zhejiang University, China *PROGRAM CHAIRS* - Étienne André, Université Sorbonne Paris Nord, France - Jingyi Wang, Zhejiang University, China - Naijun Zhan, Peking University, China *HONORABLE CHAIRS* - Jin Song Dong, National University of Singapore, Singapore - Jifeng He, Tongji University, China - Huimin Lin, Chinese Academy of Sciences, China *CONFERENCE LOCAL CHAIRS* - Xinyu Wang, Zhejiang University, China - Wenhai Wang, Zhejiang University, China *PUBLICITY CHAIRS* - Yamine Aït-Ameur, University of Toulouse, France - Jie An, Institute of Software, CAS, China *TUTORIAL CHAIR* - Dongxia Wang, Zhejiang University, China *WORKSHOP CHAIR* - Mingshuai Chen, Zhejiang University, China *FINANCIAL CHAIR* - Ling Shi, Nanyang Technological University, Singapore *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 (Chair) - Kazuhiro Ogata, JAIST, Japan - Shengchao Qin, Teesside University, UK *TOPICS OF INTEREST* 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 and with AI - Formal methods for Cyber-physical systems and IoT - Formal methods for security - Formal certification of products - Industrial case studies *IMPORTANT DATES (ANYWHERE ON EARTH)* - Abstract Submission Deadline: May 25, 2025 => 11th June 2025 - Full Paper Submission Deadline: June 1, 2025 => 15th June 2025 - Acceptance Notification: August 1, 2025 - Camera-ready Paper Submission Deadline: August 20, 2025 - Conference: November 10-13, 2025 *SUBMISSION GUIDELINES* Submission should be done through the ICFEM 2025 submission page. As in previous years, the proceedings will be published in the Springer Lecture Notes in Computer Science series. Papers should be written in English in the Springer's LNCS format. Formatting style files and further guidelines for formatting can be found at the Springer website (more details found on https://www.springer.com/gp/computer-science/lncs/conference-proceedings-gu…. We encourage authors to add line numbers to their submissions. This can be done, for example, using the lineno LaTeX package. Main Conference Paper Submissions should not exceed 16 pages (excluding references and appendix) in Springer's LNCS format. Each submission will undergo a rigorous single-blind peer-review process by at least three experts. Doctoral Symposium seeks students' submissions in two categories: (1) 2-page extended abstracts which will not be included in the proceedings; (2) 6-page papers which will be included in the proceedings. The authors with accepted submissions are expected to present their work at the symposium. Journal-first Presentations invite interested researchers to submit a short proposal for their recently published journal articles, providing the authors an opportunity to speak directly to the community. Even though there will be no artifact evaluation at ICFEM this year, we encourage authors to upload their artifacts to an archive such as Zenodo or GitHub to ensure reproducibility and availability. *CONTACT INFORMATION* For any questions regarding submissions, please email the program chairs. For more information, please visit: https://icfem2025.github.io

1 0

Formal Methods Update Meeting 2025
by Kumar Madhukar 24 May '25

24 May '25

Dear all, The Formal Methods Update Meeting 2025 will be held as a physical meeting at DA-IICT in Gandhinagar during 3–4 July, 2025. Please visit the website https://fmindia.cmi.ac.in/update2025/ for registration and other details. The FM Update Meeting is an informal event organized by the FM community in India annually, with the aim of getting FM researchers together to present and discuss topical developments in their areas of interest. Everybody interested in the use of Formal Methods in Program Design and Verification and Theoretical Computer Science is welcome to join. If you would like to give a talk at the meeting, please send us a title and an abstract of your talk to fmupdatemeet(a)gmail.com. Best regards, Organizing Committee, FM Update Meeting 2025

1 0

Deadline extended: Six PhD positions on "Cyclic Structures in Programs and Proofs" (The Netherlands, different locations)
by Jorge A. Pérez 22 May '25

22 May '25

*[Apologies for cross-posting; please forward to any good students you might know.]* We invite applications for six fully-funded PhD positions (4 years) in the project "Cyclic Structures in Programs and Proofs - New Harmonies in Software Correctness by Construction" https://cyclic-structures.gitlab.io/vacancies ===================================================== Due to several requests, the deadline for submitting applications has been extended. The new deadline is *Monday, May 26, 2025*, 23:59 (CET). ===================================================== # About the Project This €3 million project aims to advance software verification through fundamental research in the following areas: - Modal logic, proof theory, and coalgebras; - Programming languages, concurrency, and type systems; - Proof assistants (Agda, Rocq). Funded by the Dutch Research Council (NWO), this consortium brings together researchers from different universities: - Bahareh Afshari (University of Gothenburg) - Henning Basold (Leiden University) - Marcello Bonsangue (Leiden University) - Georgiana Caltais (University of Twente) - Jesper Cockx (TU Delft) - Helle Hvid Hansen (University of Groningen) - Robbert Krebbers (Radboud University Nijmegen) - Jorge Pérez (University of Groningen, Principal Investigator) # Candidate Profile We seek strong, highly motivated applicants who: - Have (or are close to completing) an MSc in Computer Science, Logic, Mathematics, or a related field. - Preferably have background or research experience in any of the areas above. - Have strong communication skills (oral and written) in English. # Position Details - The six PhD positions are fully funded, employed positions for four years. The conditions of employment follow the Collective Labour Agreement for Dutch Universities. - Candidates will be based in and employed by one of the participating universities and collaborate with national and international partners. # How to Apply For full details about the six positions and to submit your application, visit: https://cyclic-structures.gitlab.io/vacancies/ Deadline (extended): Submit your application until Monday, May 26, 2025, 23:59 (CET), for full consideration. Applications will be reviewed until all positions are filled. Starting date: We expect positions to start in September 2025 (or soon thereafter). Some flexibility is possible, depending on the position. Questions and informal inquiries: Please contact Jorge Pérez (Principal Investigator) at <j.a.perez(a)rug.nl> -- Jorge A. Pérez Associate Professor Leader, Fundamental Computing group Bernoulli Institute for Math, CS and AI University of Groningen, The Netherlands <https://www.jperez.nl> / <https://www.rug.nl/fse/fc>

1 0

IARCS Verification Seminar Series -- Talk by Sreejith A V on May 20 at 1900 hrs IST
by VSS IARCS 19 May '25

19 May '25

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Sreejith A V, a faculty member in the Department of Computer Science at IIT Goa. The talk is scheduled on Tuesday, May 20, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NHRwODlxNj…> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/) and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: Active learning of deterministic one-counter automata Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: Deterministic one-counter automata (DOCA) extend finite automata with a counter that can be incremented, decremented or reset to zero. The transition of a DOCA depends on the current state, the letter, and whether the current counter value is zero. In an active learning framework, a Learner intends to learn a language by querying the Teacher with membership and equivalence queries. Angluin's classical L* algorithm showed that in this framework, a DFA can be learnt in polynomial time. In this talk, we are interested in the active learning of DOCA. All existing algorithms for learning DOCA run in time exponential in the size of the minimal DOCA recognising the language. We present OL*, the first active learning algorithm that learns a DOCA in polynomial time. This is a joint work with Prince Mathew and Vincent Penelle. arXiv: https://arxiv.org/abs/2503.04525 (to appear in LICS'25) Bio: Sreejith A V is a faculty member in the Department of Computer Science at IIT Goa. His research interests lie in theoretical computer science, especially formal methods. In the past, he has also held research positions in University of Tubingen, TIFR - Mumbai, LIAFA - Paris, CMI - Chennai, and University of Warsaw - Poland.

1 0