FMIndia March 2025

fmindia@cmi.ac.in

4 participants
4 discussions

FMCAD 2025 - 2nd Call for Papers

by Daniela Kaufmann

================================================================================ Formal Methods in Computer-Aided Design (FMCAD) 2025 - Second Call for Papers ================================================================================ FMCAD 2025 is the twenty-fifth edition in a series of conferences on the theory and applications of formal methods in hardware and system verification. The conference encompasses a wide range of topics related to formal aspects of computer-aided system design, including verification, specification, synthesis, and testing and provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. ## General Information Conference Website: https://fmcad.org/FMCAD25/ Conference Location: SRI Headquarters, Menlo Park, California, US Conference Dates: October 6 - October 10, 2025 FMCAD 2025 includes the FMCAD Student Forum (https://fmcad.org/FMCAD25/student_forum/) and is co-located with VSTTE 2025. ## Topics of Interest FMCAD welcomes submission of papers reporting original research on advances in all aspects of formal methods and their applications to computer-aided design. Topics of interest include (but are not limited to): *Model checking, theorem proving, equivalence checking, abstraction and reduction, compositional methods, decision procedures at the bit- and word-level, probabilistic methods, combinations of deductive methods and decision procedures. *Synthesis and compilation for computer system descriptions, modeling, specification, and implementation languages, formal semantics of languages and their subsets, model-based design, design derivation and transformation, correct-by-construction methods. *Application of formal and semi-formal methods to functional and non-functional specification and validation of hardware and software, including timing and power modeling, verification of computing systems on all levels of abstraction, system-level design and verification for embedded systems, cyber-physical systems, automotive systems and other safety-critical systems, hardware-software co-design and verification, and transaction-level verification. *Experience with the application of formal and semi-formal methods to industrial-scale designs; tools that represent formal verification enablement, introduce new features, or substantially improve the automation of formal methods. *Application of formal methods to verifying safety, connectivity and security properties of networks, distributed systems, smart contracts, block chains, and IoT devices. *Application of formal methods to the analysis of machine learning systems, and applications of machine learning to enhance formal methods techniques. ## Important Dates *Abstract Submission Deadline: April 20, 2025 *Paper Submission Deadline: April 27, 2025 *Author Response: June 17 - June 19, 2025 *Author Notification: July 1, 2025 All deadlines are 11:59 pm AoE (Anywhere on Earth) ### FMCAD/VSTTE Program Outline *Main VSTTE Day: October 6, 2025 *Joint FMCAD/VSTTE Tutorial Day: October 7, 2025 *Main FMCAD days: October 8 - October 10, 2025 ## Submission Guidelines Submissions must be made electronically in PDF format via EasyChair: https://easychair.org/conferences?conf=fmcad2025 Two categories of papers are invited: Regular papers, and Tool & Case Study papers. **Regular papers*are expected to offer novel foundational ideas, theoretical results, or algorithmic improvements to existing methods, along with experimental impact validation where applicable. **Tool & Case Study papers*are expected to report on the design, implementation or use of verification (or related) technology in a practically relevant context (which need not be industrial), and its impact on design processes. Both Regular and Tool & Case Study papers must use the IEEE Transactions format on letter-size paper with a 10-point font size; preferably, use the FMCAD template for papers. Papers in both categories can be either 8 pages (long) or 4 pages (short) in length excluding references. Short papers that describe emerging results, practical experiences, or original ideas that can be described succinctly are encouraged. Authors will be required to select an appropriate paper category at abstract submission time. Submissions may contain an optional appendix, which will not appear in the final version of the paper. The reviewers should be able to assess the quality and the relevance of the results in the paper without reading the appendix. Submissions in all categories must contain original research that has not been previously published, nor is concurrently submitted for publication. Any partial overlap with published or concurrently submitted papers must be clearly indicated. FMCAD employs a rigorous peer-review process and each submission will be reviewed by at least four members of the program committee. The review process is single-blind. The review process will incorporate a feedback and rebuttal period during which authors will have the opportunity to formally respond to reviewer comments. **New - Artifact Evaluation:**FMCAD 2025 introduces optional artifact evaluation to enhance transparency and the usability of research outcomes. Authors reporting experimental results are strongly encouraged to publish their final data in a long-term repository (e.g. zenodo (https://zenodo.org)). With artifacts serving as supplementary evidence, high-quality artifacts can improve the likelihood of paper acceptance. Artifact evaluation will be integrated into the main review process, with one selected program committee member assessing the quality of the artifact alongside the paper. Accepted artifacts require a DOI and will be clearly identified in the published paper. Details are available on the Artifacts Page (https://fmcad.org/FMCAD25/cfa). Accepted papers are published by TU Wien Academic Press under a Creative Commons license (the authors retain the copyright) and distributed through the IEEE XPlore digital library. IEEE CEDA is a technical co-sponsor of FMCAD. There are no publication fees. Authors of accepted contributions will be required to sign the FMCAD copyright transfer form found here: https://fmcad.or.at/pdf/copyright.pdf. For each accepted paper, at least one unique author must register for the conference. Moreover, authors of accepted papers ensure that at least one of them will attend the conference and present the work. ## Student Forum Continuing the tradition of the previous years, FMCAD 2025 will host a Student Forum that provides a platform for graduate students at any career stage to introduce their research to the wider Formal Methods community, and solicit feedback. Submissions for the student forum must be short reports describing research ideas or ongoing work that the student is currently pursuing, and must be within the scope of FMCAD. Work that has been partly published previously might be considered; the novel aspect to be addressed in future work must be clearly described in such cases. All submissions will be reviewed by a selected group of FMCAD student forum committee members. Details are available on the Student Forum Page (https://fmcad.org/FMCAD25/student_forum). ## FMCAD 2025 Committees ### Program Chair Ahmed Irfan, SRI, CA, USA Daniela Kaufmann, TU Wien, Austria ### Program Committee Guy Amir, Cornell University Erika Ábrahám, RWTH Aachen University Kshitij Bansal, Google Haniel Barbosa, Universidade Federal de Minas Gerais Per Bjesse, Synopsys Inc. Nikolaj Bjørner, Microsoft Martin Blicha, University of Lugano Roderick Bloem, Graz University of Technology Rayna Dimitrova, CISPA Helmholtz Center for Information Security Supratik Chakraborty, IIT Bombay Aleksandar Chakarov, Phase Change Software LLC Pascal Fontaine, Université de Liège Katalin Fazekas, TU Wien Divya Gopinath, NASA Ames (KBR Inc.) Alberto Griggio, Fondazione Bruno Kessler Arie Gurfinkel, University of Waterloo Liana Hadarean, Amazon Web Services Paula Herber, University of Münster Osman Hasan, National University of Sciences and Technology (NUST) Marijn Heule, Carnegie Mellon University Antti Hyvarinen, Certora Alexey Ignatiev, Monash University Mitesh Jain, Rivos Inv. Mikolas Janota, Czech Technical University in Prague Susmit Jha, SRI International Martin Jonas, Masaryk University Jianwen Li, East China Normal University Enrico Magnago, Amazon Web Services Sergio Mover, Ecole Polytechnique Antonina Nepeivoda, Program System Institute of RAS Aina Niemetz, Stanford University Mathias Preiner, Stanford University Stefan Ratschan, Czech Academy of Sciences Kristin Rozier, Iowa State University Philipp Rümmer, University of Regensburg and Uppsala University Mark Santolucito, Barnard College Christoph Scholl, University of Freiburg Martina Seidl, Johannes Kepler Univeristy Linz Natarajan Shankar, SRI International Natasha Sharygina, University of Lugano Anna Slobodova, ARM Mate Soos, Ethereum Foundation Christoph Sticksel, The MathWorks Nestan Tsiskaridze, Stanford University Ashish Tiwari, Microsoft Georg Weissenbacher, TU Wien Andrew Wu, Amherst College Nisansala Yatapanage, Australian National University Emily Yu, Institute of Science and Technology Austria Cunxi Yu, University of Maryland Zhen Zhang, Utah State University Hongce Zhang, Hong Kong University of Science and Technology (Guangzhou) Yoni Zohar, Bar-Ilan University ### Local Chair Stéphane Graham-Lengrand, SRI, CA, USA ### Registration Chair Jenny McNeill, SRI, CA, USA ### Student Forum Chairs Tanja Schindler, University of Basel, Switzerland Lee A. Barnett, AWS, CA, USA ### Sponsorship Chair: Alex Ozdemir, Stanford University, CA, USA ### Publication Chair Georg Weissenbacher, TU Wien, Austria ### Web Chair Thomas Hader, TU Wien, Austria ### FMCAD Steering Committee Clark Barrett, Stanford University, CA, USA Armin Biere, University of Freiburg, Germany Ruzica Piskac, Yale University, USA Anna Slobodova, ARM, USA Georg Weissenbacher, TU Wien, Austria

2 days, 18 hours

IARCS Verification Seminar Series -- Talk by Alastair Donaldson on March 4 at 1900 hrs IST

by VSS IARCS

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Alastair Donaldson, a Professor and Director of Research in the Department of Computing at Imperial College London. The talk is scheduled on Tuesday, March 4, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=Nzd2Zmc1bn…> ). 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: Taking Back Control: Formally Modelling a Compiler Intermediate Representation for GPU Computing Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: We will present our POPL 2023 work on using formal modelling and analysis techniques to understand and fix fundamental problems in the design of SPIR-V, a compiler intermediate representation that is widely-used in GPU computing. An innovation of SPIR-V is that it features special instructions that allow information about high level control flow constructs to be documented in its otherwise-unstructured basic block-based representation. The idea is that compilers can exploit this information to generate efficient GPU-specific machine code. However, the original definitions of these instructions and the rules that govern them were fraught with ambiguities, preventing users of SPIR-V from understanding their purpose and hindering their use by compiler developers. We used the Alloy modelling language and analysis tool to build an initial best-effort formal model of SPIR-V control flow, after which we iteratively refined the model by cross-checking it against official documentation, test suites and validation tools, consulting with experts in industry to resolve differences. Along the way we fixed numerous deficiencies in these test suites and validation tools, and ended up with agreement between our revised formal model and these other sources of truth about SPIR-V. We then rewrote relevant parts of the English language formal specification based on our rigorous formal model, and our changes to the language have been incorporated in the latest version of the SPIR-V specification. As an added bonus, we devised a novel technique for automated testing of SPIR-V compilers that uses our formal model to generate unusual control flow graphs which are then fleshed out into self-checking SPIR-V test cases. This led to the discovery of numerous bugs affecting open source and commercial SPIR-V compilers. Bio: Alastair Donaldson is a Professor in the Department of Computing at Imperial College London where he is Director of Research and leads the Multicore Programming Group, investigating novel techniques and tool support for programming, testing and reasoning about highly parallel systems and their programming languages. He was Founder and Director of GraphicsFuzz Ltd., a start-up company specialising in metamorphic testing of graphics drivers, which was acquired by Google in 2018, after which he spent time working with Google as a software engineer and then as a Visiting Researcher. He was the recipient of the 2017 BCS Roger Needham Award and an EPSRC Early Career Fellowship, and has published more than 100 articles in the fields of programming languages, formal verification, software testing and parallel programming. Alastair was previously a Visiting Researcher at Microsoft Research Redmond, an EPSRC Postdoctoral Research Fellow at the University of Oxford and a Research Engineer at Codeplay Software Ltd. He holds a PhD from the University of Glasgow, and is a Fellow of the British Computer Society.

5 days, 11 hours

CFP: 1st Workshop on Hot Topics in Distributed Machine Learning @ IEEE ICDCS 2025. Deadline: March 16th, 2025

by HotDiML-Workshop

---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Our apologies if you receive multiple copies of this CFPs. We would appreciate your help to contribute & forward this CFPs to your friends. ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Dear Colleagues, We are honored that IEEE ICDCS 2025 (https://icdcs2025.icdcs.org <https://icdcs2025.icdcs.org/>) will be hosting the 1st Workshop on Hot Topics in Distributed Machine Learning (HotDiML) this year! HotDiML provides researchers working in the Distributed Machine Learning field with a platform for critical thinking, sharing both successes and failures, and fostering constructive discussions. The workshop encourages novel directions, accepting papers that offer fresh perspectives or critical analyses, even if not fully developed. These papers can provide valuable insights to advance the field. We invite you to contribute with your recent work presented as position, research, experimental evaluation or report papers on Distributed Machine Learning. The accepted papers will be presented at the workshop and a plenary discussion will be held alongside these presentations. Please check the call for paper here: https://hotdiml.github.io/HotDiML2025/cfp/. Important Dates: Deadline for submissions: March 16th, 2025 Notification of acceptance: April 2nd, 2025 Camera-ready: April 16th, 2025 Workshop days: July 20th, 2025 Important Note: For each accepted paper, at least one author is required to register and attend the workshop in-person to present their paper on-site. No-show paper will be reported to the publisher and removed from the ICDCSW companion conference proceedings. All accepted and presented papers will be included in the IEEE ICDCSW companion conference proceedings and IEEE digital library. Note that the authors should adhere to ethic and professional standards of IEEE. Please refer to IEEE Code of Ethics and IEEE Policy of AI-Generated Text. We look forward to your submission and the eventual inspiring conversations in Glasgow, Scotland, UK! All the best! HotDiML 2025 Organizers Andrea Agiollo, Enkeleda Bardhi, Paolo Bellavista, Rajiv Khanna and Riccardo Lazzeretti hotdiml.workshop(a)gmail.com <mailto:hotdiml.workshop@gmail.com>

5 days, 13 hours

Postdoc in Verification and Game Theory at the University of Liverpool

by Patrick Totzke

(apologies for the cross-posting!) Dear colleagues, Hi all, we are looking for a postdoc interested in games on graphs, automata/logics, and generally game theory, to join the verification group at the University of Liverpool. The post is for two years and is to be filled as soon as possible (there is some flexibility). The application deadline is 2025-03-30. All details here: <https://my.corehr.com/pls/ulivrecruit/erq_jobspec_version_4.display_form?p_…> Thanks and best wishes, P

5 days, 14 hours

2025

2024

2023

2022

FMIndia March 2025