- FMIndia - example.com

IARCS Verification Seminar Series -- Talk by Nikhil Swamy on April 8 at 1900 hrs IST

by VSS IARCS

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Nikhil Swamy, a researcher at Microsoft Research in Redmond. The talk is scheduled on Tuesday, April 8, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=Mm5wcm80ZW…> ). 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: Pulse: Proof-oriented Programming with Concurrent Separation Logic in F* Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: F* is a dependently typed programming language. It has been used to develop more than a million lines of verified code and proofs, for artifacts ranging from cryptographic libraries to networking components. Some of this verified software runs in widely used production systems, ranging from the Windows kernel to the Python standard library. However, most of this corpus of verified code is purely sequential. Pulse is a new extension of F* enabling programming and proving imperative programs with shared-memory concurrency. Proofs in Pulse are conducted in a new program logic called PulseCore, a concurrent separation logic with state-of-the-art features, including higher-order ghost state and impredicative invariants, backed by a foundational semantics developed within F* itself. Programs are verified in Pulse using a custom checker with a combination of tactics and SMT solving. Once proven, programs in Pulse can be extracted to OCaml, C, or Rust, depending on the libraries and features used. Pulse is being used in a number of new projects, including in the development of verified firmware, in new libraries for secure data formatting, and for verified CPU/GPU programs. I will provide some background on F* and concurrent separation logic, and then introduce Pulse by way of examples and a tool demonstration. Bio: Nikhil Swamy is a researcher at Microsoft Research in Redmond, working in the Research in Software Engineering (RiSE) group. He is interested in type systems, program logics, functional programming, program verification and interactive theorem proving, and also in the use of these techniques to build provably secure programs, including web applications, web browsers, crypto protocol implementations, and low-level systems code.

11 months, 1 week

1
0
0 0

Waklert 150 Mg: Best Solution For People With Chronic Fatigue | cheaptrustedpharmacy

by ameliasmith7891＠gmail.com

Waklert 150mg effectively fights chronic fatigue by stimulating neurotransmitters responsible for alertness and energy production. Waklert 150 is an effective solution for managing chronic fatigue, excessive tiredness, and cognitive sluggishness. Whether you're a professional, student, shift worker, or someone with a sleep disorder, this medication can help you stay energized, focus, and productive. Fatigue often leads to brain fog and reduce concentration. Waklert enhances focus, memory, and problem-solving skills, making it easier to stay on top of tasks. By optimizing dopamine levels, Waklert 150 mg supports emotional well-being, reducing stress and anxiety linked to fatigue. It is widely prescribed for sleep disorders like narcolepsy, obstructive sleep apnea , and shift work sleep disorder but is also used off-label for energy enhancement and fatigue management. Visit Here : https://www.cheaptrustedpharmacy.com/product/waklert-150-australia/

11 months, 1 week

1
0
0 0

Lead Software Engineer position in FV tool - Jasper/Cadence

by Ravi Prakash

Hi, We have an open position in industry leading formal product Jasper from Cadence. The position is in Bangalore and we are interested in recently completed PhDs or a Masters in formal domain. Looking for people who are passionate about formal/coding and making an impact with their knowledge in Jasper. Please write to me directly at ravipr(a)gmail.com or ravipr(a)cadence.com for further details. Thanks Ravi

11 months, 1 week

1
0
0 0

Webinar on logic education

by Madhavan Mukund

----- Forwarded message from R Ramanujam <jam(a)imsc.res.in> ----- From: R Ramanujam <jam(a)imsc.res.in> The DLMPST Commission on Logic Education https://dlmps.org/pages/commissions.php invites you to a webinar on logic education by Professor Maria Manzano. Date: Apr 8, 2025 Time: 1000 EST, 1200 GMT, 1400 CET, 1930 IST, 2200 (Beijing) Zoom link: https://cmi-ac-in.zoom.us/j/89497108451?pwd=rLl7QvAfnfJHTxp5h6ZVoZzyGuvNQQ.1 Meeting ID: 894 9710 8451 Passcode: udayana Talk details: Tools for teaching logic Maria Manzano Salamanca, Spain I will tell you about the European ALFA project on Tools for Teaching Logic that we had last century and about the International TTL Congresses that we held in 2000, 2006, 2011, 2015, and 2023. The first goal of the ALFA project was to share our experience as teachers among Aracne members. We proposed: (1) the preparation of a metabook (with hypertext version), (2) the design of an on-line dictionary of logic terms, (3) the investigation of the existing software for the teaching of logic, (4) the translation of both elementary and interdisciplinary texts and software, (5) to help potential authors to write lecture notes, (6) the dissemination of our project both within our academic community and outside it (high school), thus bolstering a good image of Logic and (7) to support women’s participation in higher education. The network we created was interdisciplinary and included professors and researchers from philosophy, mathematics, computer science, and linguistics. Some of the results of the project can be consulted on the Aracne website (aracne.usal.es.) and others in the Summa Logicae digital library (logicae.usal.es) Speaker Bio: María Gracia Manzano Arjona is a Spanish philosopher specializing in mathematical logic and model theory. Manzano earned her Ph.D. in 1977 from the University of Barcelona. Her dissertation, Sistemas generales de la lógica de segundo orden [General systems of second-order logic], was supervised by Jesús Mosterín. She is a professor of logic and the philosophy of science at the University of Salamanca. She is the author of several books on logic and model theory. https://en.wikipedia.org/wiki/Mar%C3%ADa_Manzano -- R Ramanujam ----- End forwarded message -----

11 months, 1 week

1
0
0 0

Call For Papers - APLAS 2025, Bengaluru, India

by Madhavan Mukund

----- Forwarded message from Pritam Gharat <pritamgharat(a)microsoft.com> ----- From: Pritam Gharat <pritamgharat(a)microsoft.com> To: "fmindia-owner(a)cmi.ac.in" <fmindia-owner(a)cmi.ac.in> Date: Wed, 26 Mar 2025 11:02:46 +0000 Subject: Call For Papers - APLAS 2025, Bengaluru, India CALL FOR PAPERS: The 23rd Asian Symposium on Programing Languages and Systems (APLAS 2025) 27-30 October 2025, Bangalore, India APLAS 2025 - The 23rd Asian Symposium on Programming Languages and Systems - APLAS 2025<https://conf.researchr.org/track/aplas-2025/aplas-2025-aplas-2025> AIM AND SCOPE: APLAS 2025 is the 23rd in a series of symposia that solicits submissions in the form of regular research papers describing original scientific research results, including system development and case studies. Among others, solicited topics include: * Programming paradigms and styles: functional, object-oriented, probabilistic, logic, constraint programming; extensible programming languages; programming languages for systems code; novel programming paradigms; * Methods and tools to specify and reason about programs and languages: programming techniques; meta-programming; domain-specific languages; proof assistants; type systems; dependent types; program logics, static and dynamic program analysis; language-based security; model checking; testing; * Programming language foundations: formal semantics; type theory; logical foundations; category theory; automata; effects; monads and comonads; recursion and corecursion; continuations and effect handlers; program verification; memory models; abstract interpretation; * Methods and tools for implementation: compilers; program transformations; rewriting systems; partial evaluation; virtual machines; refactoring; intermediate languages; run-time environments; garbage collection and memory management; tracing; profiling; build systems; program synthesis; * Concurrency and distribution: process algebras; concurrency theory; session types; parallel programming; service-oriented computing; distributed and mobile computing; actor-based languages; verification and testing of concurrent and distributed systems; * Applications and emerging topics: programming languages and PL methods in education, security, privacy, database systems, computational biology, signal processing, graphics, human-computer interaction, computer-aided design, artificial intelligence and machine learning; case studies in program analysis and verification. IMPORTANT DATES (all deadlines in AoE): * Paper submission deadline: April 18, 2025 * Tutorials and Workshops: October 27, 2025 * Conference: October 28 – October 30, 2025 SUBMISSIONS: APLAS welcomes submissions that should not exceed 17 pages, excluding bibliography, in the Springer LNCS format. Additional material intended for reviewers but not for publication in the final version -– for example, details of proofs -– may be placed in a clearly marked appendix that is not included in the page limit. However, the paper must be understandable without the appendix. Reviewers are not obligated to review it. Papers should be submitted via HotCRP: https://aplas25.hotcrp.com/ GENERAL CHAIR: Pritam Gharat, Microsoft Reasearch, India, pritamgharat(a)microsoft.com<mailto:pritamgharat@microsoft.com><mailto:pritamgharat@microsoft.com%3cmailto:pritamgharat@microsoft.com%3e> LOCAL ORGANIZATION CHAIR: Sujit Kumar Chakrabarti, IIIT-Bangalore, India, sujitkc(a)iiitb.ac.in<mailto:<mailto:pritamgharat@microsoft.com%3cmailto:pritamgharat@microsoft.com%3e>sujitkc(a)iiitb.ac.in><mailto:pritamgharat@microsoft.com%3cmailto:pritamgharat@microsoft.com%3e> PROGRAM CHAIRS: Alex Potanin, Australian National University, Alex.Potanin(a)anu.edu.au<mailto:<mailto:pritamgharat@microsoft.com%3cmailto:pritamgharat@microsoft.com%3e>Alex.Potanin(a)anu.edu.au><mailto:pritamgharat@microsoft.com%3cmailto:pritamgharat@microsoft.com%3e> PROGRAM COMMITTEE: Alex Potanin, Australian National University Alexander Bakst, Certora Swarnendu Biswas, IIT Kanpur Andreea Costea, TU Delft Meenakshi D'Souza, IIITB - International Institute of Information Technology Bangalore Jeffrey S. Foster, Tufts University Kihong Heo, KAIST Zhenjiang Hu, Peking University Atsushi Igarashi, Kyoto University Stephen Kell, King's College London Oleg Kiselyov, Tohoku University V Krishna Nandivada, IIT Madras Liyi Li, Iowa State University Umang Mathur, National University of Singapore Kartik Nagar, IIT Madras Liam O'Connor, Australian National University Lionel Parreaux, HKUST (The Hong Kong University of Science and Technology) Sanjiva Prasad, Indian Institute of Technology Delhi G. Ramalingam, Microsoft Ina Schaefer, KIT KC Sivaramakrishnan, IIT Madras and Tarides Tachio Terauchi, Waseda University Manas Thakur, IIT Bombay Pascal Weisenburger, University of St. Gallen ----- End forwarded message -----

11 months, 2 weeks

1
0
0 0

How Modalert 200mg Helped Me Stay Awake & Focused

by romankenndy＠gmail.com

As someone who struggled with daytime sleepiness and lack of focus, I needed a real solution. After researching, I decided to try Buy Modalert 200mg online, and the results were incredible. Unlike caffeine, which gave me short bursts of energy followed by crashes, Modalert provided sustained alertness and mental clarity throughout the day. How It Changed My Routine No More Fatigue – I could work for hours without feeling mentally drained. Enhanced Focus – Tasks that required deep concentration became much easier to handle. Improved Memory & Cognitive Sharpness – I processed information faster and retained details better. Smooth & Side Effect-Free – No jitters, anxiety, or sudden crashes. Who Can Benefit? Students & professionals need sharper focus. Night shift workers struggle with irregular sleep. People with sleep disorders like narcolepsy or sleep apnea. If you want to buy Modalert 200mg in Australia, choose a trusted pharmacy. My go-to is Generic Pills Australia—they offer genuine products, secure payments, and fast delivery. This has been a life-changing solution for my productivity! https://www.genericpillsaustralia.com/product/modalert-200-australia/

11 months, 3 weeks

1
0
0 0

Senior Project Associate/Postdoc Position - Model Checking/Formal Verification/Software Engineering

by Arpit Sharma

Dear All, Hope this email finds you well. I am writing this email to inform you that a senior project associate/postdoc position is available in my research group at IISER Bhopal in the area of model checking/formal verification/software engineering. This position is funded by the DST-SERB Core Research Grant project titled: GALTOSM: A Graph and Logic Transformation Based Toolkit for Software Model Checking. I would request you to please share this information with your PhD/Postdoc students, and colleagues in academia. Candidates with a master's degree + 2 years of relevant research/industry experience or bachelor's degree + 4 years of relevant research/industry experience are also eligible and encouraged to apply. Interested candidates can directly contact me at : arpit(a)iiserb.ac.in The details of this position are as follows: No. of Position: 1 (One) Name of Position: Senior Project Associate Duration: Initially for 1 year, extendable up to 1 year based on satisfactory performance. *Salary: INR 57,000 + HRA* (as applicable) per month. *Essential Qualifications:* Doctoral Degree in Computer Science/Computer Engineering/Software Engineering/Data Science from a recognized University or equivalent. *OR* Bachelor's degree in Engineering or Technology (B.E. or B.Tech) in Computer Engineering/Information Technology/Data Science/Electronics or four years Bachelor’s degree in Computer Science/Mathematics/Physics/Electronics or Master of science (MSc) degree in Computer Science/Data Science/Information Technology/Electronics/Mathematics/Physics from a recognized University or equivalent and four years' experience in Research and Development in computer science (preferably in software design and development or machine learning/natural language processing or formal methods/model checking) in Industrial and Academic Institutions or Science and Technology Organisations and Scientific activities and services. * OR* Master’s degree in engineering or technology (M.E. or M.Tech) in Computer Engineering or Computer Science or Software Engineering or Information Technology or Data Science or Electronics Engineering from a recognized University or equivalent and two years’ experience in Research and Development in computer science (preferably in software design and development or machine learning/natural language processing or formal methods/model checking) in Industrial and Academic Institutions or Science and Technology Organisations and Scientific activities and services. *Desirable: * 1. Candidates should have some prior experience in Software Design and Implementation or development of Software Tools or building Machine Learning Pipelines. 2. This position requires good analytical and reasoning skills. *Age limit:* Candidates should be below 50 years of age on the last date of application. *How to Apply:* Interested candidates are requested to send their CV (including name, date of birth, photograph, address for communication, phone number, email id, details of educational and scientific accomplishments) to Dr. Arpit Sharma over email. Additionally, a copy of all the credentials including mark sheets starting from 12th standard, and UG degree certificate, PG degree certificate, doctoral degree certificate etc also need to be sent via email. Completed applications should reach the undersigned only by email. Last date of application is 06th April 2025. Keep subject of the email to be “Senior Project Associate Application”. Thanks. Regards, Arpit Arpit Sharma Associate Professor Department of Electrical Engineering & Computer Science Indian Institute of Science Education and Research, Bhopal Bhopal - 462066, Madhya Pradesh, India Homepage : https://sites.google.com/iiserb.ac.in/arpit-sharma/

11 months, 3 weeks

1
0
0 0

CFP： Special Issue of Journal of Systems Architecture on Security and Privacy in AIoT-enabled Smart Cities

by Qin Liu

Special Issue of Journal of Systems Architecture on Security and Privacy in AIoT-enabled Smart Cities https://www.sciencedirect.com/special-issue/313735/security-and-privacy-in-… In a smart city, numerous artificial intelligence of things (AIoT) communicate and collaborate to improve our quality of life. Both artificial intelligence (AI) and Internet of things (IoT) are foundational technologies that have been interacting with each other to realize a smart life. As massive amounts of sensitive data are generated, processed, and exchanged through IoT devices and AI technologies, one of the fundamental problems is how to provide intelligent services in smart cities without compromising security and privacy. This special issue aims to bring together researchers and practitioners in IoT, AI, and network security, to share their novel ideas and latest findings in relation to security and privacy in AIoT-enabled smart cities. The scope and interests for the special issue include, but are not limited to, the following list: ● Secure IoT infrastructure for smart cities ● Secure smart city applications, including secure AI-driven IoT applications ● Authentication and access control in IoT-enabled smart cities ● Intrusion detection for IoT-enabled smart cities ● Architectures and standards for secure IoT systems ● AI and big data techniques for IoT-enabled secure smart cities ● Blockchain technology for IoT-enabled secure smart cities ● Secure multi-party computation techniques for ML ● Security optimization in heterogeneous environments ● AI-driven mechanisms and models to perform attacks ● Security and privacy issues in AI-enabled IoT communications and systems ● Privacy-preserving ML ● Privacy-preserving data mining ● Privacy and anonymity techniques for IoT and AI ● Data privacy in AIoT-enabled smart cities ● Privacy preserving techniques for IoT-enabled smart cities ● Privacy modeling and analysis for IoT-enabled smart cities ● Miscellaneous privacy issues in AIoT-enabled smart cities Important Dates Submissions Deadline: April 1, 2025; First-round pass notification: April 15, 2025; Review result notification: June 1, 2025; Acceptance/rejection: August 30, 2025; Publication: 2nd Quarter 2025 Submission Format and Guideline Authors should follow the "Guidelines for Authors" from The Journal of Systems Architecture (JSA). Details can be found at Guide for authors - Journal of Systems Architecture (https://www.sciencedirect.com/journal/journal-of-systems-architecture/publi…). Solicited original submissions must not be currently under consideration for publication in other venues. All manuscripts and any supplementary material should be submitted through Submission site for Journal of Systems Architecture ( https://www.editorialmanager.com/jsa/default.aspx). Please select the “VSI:SPASS” option as article type of the paper. Guest editors: Associate Prof. Qin Liu Hunan University, Changsha, China Prof. Kouichi Sakurai Kyushu University, Fukuoka, Japan Prof. Richard Hill University of Huddersfield, Huddersfield, UK Associate Prof. Wenjia Li UK New York Institute of Technology, Old Westbury, USA -- Dr. Qin Liu College of Computer Science and Electronic Engineering Hunan University Changsha, Hunan Province,P.R. China, 410082 Mobile: +86-13548577157 Email: gracelq628(a)hnu.edu.cn; gracelq628(a)126.com Homepage: https://qinliu-hnu.github.io/

12 months

1
0
0 0

NETYS 2025 - Extended deadline

by Madhavan Mukund

*** The submission deadline for NETYS is extended to 15 March, 2025 *** Call for Papers THE 13th INTERNATIONAL CONFERENCE ON NETWORKED SYSTEMS (NETYS 2025) 21-23 May, 2025, Rabat, Morocco http://www.netys.net AIM AND SCOPE NETYS aims to bring together researchers and engineers from the theory and practice of distributed and networked systems. The scope of the conference covers all aspects related to the design and the development of these systems, including, but not restricted to, cloud systems, formal verification, concurrent and distributed algorithms, data management, data science, parallel/concurrent/distributed programming, machine learning theory and applications, large language models, multicore architectures, networks, and security. NETYS will provide a forum to report on best practices, novel algorithms, results, and techniques on networked systems. Original research contributions and experience papers on the principles, design, implementation, modeling, analysis, verification and application of networked systems are solicited. Topics of interest are broadly divided into three categories: networked systems, distributed computing and machine learning. Topics of interest include (but are not limited to): 1. NETWORKED SYSTEMS - Cloud systems and data centers - Cyber-physical systems - Distributed database, embedded and operating systems - Multicore architectures and multithreaded applications - Distributed ledgers and blockchain technologies - Internet of Things, 5G, URLLC - Mobile, wireless, ad-hoc and sensor networks - Social networks - Overlay and peer-to-peer infrastructures 2. DISTRIBUTED COMPUTING - Concurrency, synchronization and persistence - Distributed and concurrent data structures - Languages, verification and formal methods for distributed systems - Design and analysis of distributed algorithms - Lower bounds and impossibility results for distributed computing - Game theory, mechanisms design - Fault-tolerance, reliability, self-stabilizing, self-organizing, and autonomic systems - Collaborative intelligent systems 3. MACHINE LEARNING - Collaborative/federated learning - Distributed Machine learning - Trustworthy machine learning - Large language models theory and applications - Fairness and privacy in machine learning - Reinforcement learning theory and applications - Generative AI - Optimization algorithms IMPORTANT DATES (all deadlines are at 23:59 AoE) - Abstract submission: March 15th, 2025 - Paper submission: March 15th, 2025 - Notifications: April 14th, 2025 - Conference dates: May 21st-23rd, 2025 INVITED SPEAKERS - Swarat Chaudhuri (University of Texas & Google DeepMind, Austin, USA) - Mohamed El Amine Seddik (Technology Innovation Institute, AD, UAE) - Sanjit Seshia (University of California, Berkeley, USA) - Marc Shapiro (Sorbonne Universite, Paris, France) - Praneeth Vepakomma (MBZUAI, Abu Dhabi, UAE & MIT, Cambridge, USA) PUBLICATION Springer's Lecture Notes in Computer Science series will publish conference proceedings (https://www.springer.com/gp/computer-science/lncs). One of the authors of each accepted paper must present it at the conference. SUBMISSION INSTRUCTIONS All submissions must follow the LNCS template and be written in English. Full papers are allowed a maximum of 15 pages in the LNCS format, excluding bibliographic references, whereas short papers are allowed a maximum of 5 pages (in the same format). Papers exceeding these limits may be rejected without review. A clearly marked appendix can be included for supplementary materials, but it will be read at the reviewers' discretion; therefore, the main body of the paper should contain sufficient details to assess its contributions. Submission of papers is via Microsoft CMT: https://cmt3.research.microsoft.com/NETYS2025/ PROGRAM CHAIRS Madhavan Mukund <madhavan(a)cmi.ac.in> Salem Lahlou <salem.lahlou(a)mbzuai.ac.ae> PROGRAM COMMITTEE El Mehdi Achour (RWTH Aachen University, Germany) S Akshay (IIT Bombay, India) Reda Alami (Technology Innovation Institute, UAE) Robert Basmadjian (University Mohammed VI Polytechnique, Ben Guerir, Morocco) Yahya Benkaouz (Mohammed V University, Rabat, Morocco) Mahmoud El Hamlaoui (ENSIAS, Morocco) Bernd Freisleben (Philipps-Universität Marburg, Germany) Eduard Gorbunov (Mohamed bin Zayed University of Artificial Intelligence, UAE) Loic Helouet (University Rennes, Inria, CNRS, IRISA, France) Alex Hernandez-Garcia (University of Montreal and Mila – Quebec AI Institute, Canada) Zahi Jarir (Cadi Ayyad University, Marrakech, Morocco) Mohamed Jmaeil (University of Sfax, Tunisia) Mohamed Amine Koulali (National School of Applied Sciences of Oujda, Morocco) Salem Lahlou (Mohamed bin Zayed University of Artificial Intelligence, UAE (Co-chair)) Tongliang Liu (University of Sydney, Australia) Nils Lukas (Mohamed bin Zayed University of Artificial Intelligence, UAE) Anisur Rahaman Molla (Indian Statistical Institute, Kolkata, India) Madhavan Mukund (Chennai Mathematical Institute, India (Co-chair)) Andreas Podelski (University of Freiburg, Germany) Maria Potop-Butucaru (LIP6, Sorbonne University, France) Sergio Rajsbaum (UNAM, Mexico) Mohamed El Amine Seddik (Technology Innovation Institute, UAE) Pradeep Sharma (ServiceNow, USA) B Srivathsan (Chennai Mathematical Institute, India) Afaf Taik (Mila – Quebec AI Institute, Canada) Sebastien Tixeuil (LIP6, Sorbonne University, France) Ahmed Touati (Meta AI, France) Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA)

1 year

1
0
0 0

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

1 year

1
0
0 0

2026

2025

2024

2023

2022

FMIndia