September 2025 - FMIndia

FM 2026 Tutorials: 1st Call for Tutorials

by Neeraj Kumar Singh

***************************************************************************************** FM 2026 Tutorials: Call for Tutorials https://conf.researchr.org/track/fm-2026/fm-2026-tutorials ***************************************************************************************** ## Overview FM 2026 is the 27th international symposium on Formal Methods in a series organized by Formal Methods Europe (FME), an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The FM symposia have been successful in bringing together researchers and industrial users around a program of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral research. We are inviting proposals for tutorials to complement the main FM 2026 symposium. The primary goal of these tutorials is to convey ideas with a focus on pedagogy over technical innovation. They offer a valuable platform for participants to discuss technical challenges, exchange research concepts, explore educational strategies, and demonstrate or investigate practical applications. Tutorials should be designed to be broadly accessible and pedagogically oriented, clarifying key concepts, building intuition, and ensuring ease of understanding. They aim to attract new researchers, serve as bridges to practitioners, and disseminate useful ideas widely. These may be driven by fundamental academic interests, or by needs from specific application domains. We encourage a diversity of topics relating to different ways of developing and using formal methods as well as all theoretical aspects of software engineering, including complex applications. Although tutorials focused on tools are a traditional choice, tutorials covering techniques are also welcome. Authors interested in proposing different types of tutorials are encouraged to contact the chairs for guidance. Overall, we welcome a broad range of tutorial topics, as long as they are relevant to the interests of the formal methods community. Moreover, we also invite topics at the intersection of machine learning and formal methods due to the growing interest in AI and machine learning-based software development. Accepted tutorial papers will be published in the conference proceeding volume. Authors of these papers will be allocated a presentation slot during the tutorial sessions prior to the main conference. When submitting tutorial papers, authors should indicate their preferred presentation length, which can be either half a day or a full day. ##Important Dates - Submission Deadline: February 02, 2026 (AoE) - Acceptance Notification: February 28, 2026 - Camera-ready versions: March 13, 2026 More information can be found on the website of FM 2026: https://conf.researchr.org/track/fm-2026/fm-2026-tutorials ## Submission Instructions Submission should be done through the FM 2026 submission page, handled by the EasyChair conference system: https://easychair.org/conferences/?conf=fm2026 As in previous years, the proceedings will be published in the Springer Lecture Notes in Computer Science series. Tutorial papers can be at most 25 pages in LNCS format (including references and appendices). There is no minimum length; the tutorial should be as long as necessary to be effective, but should avoid filler. Tools should include links and descriptions of how to run them. The paper must provide clear references to the original technical content and they are welcome to include an appendix for better details. Formatting style files and further guidelines for formatting can be found at the Springer website (more details: https://www.springer.com/gp/computer-science/lncs/conference-proceedings-gu…). ## Tutorials Co-Chairs - Kazuhiro Ogata, Japan Advanced Institute of Science and Technology, Japan - Neeraj Kumar Singh, INPT-ENSEEIHT/IRIT, University of Toulouse, France

1 day, 22 hours

1
1
0 0

APLAS-ATVA 2025 Call for Participation

by Madhavan Mukund

----- Forwarded message from Deepak D'Souza <deepakd(a)iisc.ac.in> ----- From: Deepak D'Souza <deepakd(a)iisc.ac.in> Date: Wed, 24 Sep 2025 06:48:04 +0000 Subject: APLAS-ATVA 2025 Call for Participation APLAS-ATVA 2025 Call for Participation The 23rd editions of the Asian Symposium on Programming Languages and Systems (APLAS 2025) and the International Symposium on Automated Technology for Verification and Analysis (ATVA 2025) will be jointly held at the International Institute for Information Technology, Bangalore (IIIT Bangalore), during 27-31 October 2025. Registrations are now open. Early Registrations close on 30th September 2025. Key highlights of the conferences include: * Invited talks by Aarti Gupta (Princeton U), Peter Mueller (ETH Zurich), and Rahul Sharma (Microsoft Research India) * APLAS and ATVA contributed Research and Tool talks * Tutorials on Replicated Data Types by Kartik Nagar (IIT Madras) and Quantitative and Probabilistic Verification by Benjamin Kaminski (Saarland U) * New Ideas and Emerging Results in Programming Languages and Systems (NIER) Track talks. * Workshop on Milestones and Motifs in Automata and Concurrency, with invited talks by Ahmed Bouajjani (Paris Diderot U), Pavithra Prabhakar (Kanas State U), P S Thiagarajan (UNC Chapel Hill), and Pascal Weil (U Sorbonne Paris Nord). A limited number of travel grants are available, particularly for students. Travel grant applications close on 05 October 2025. For more details visit the conference webpages at https://conf.researchr.org/home/atva-2025 and https://conf.researchr.org/home/aplas-2025. Deepak D'Souza and Pritam Gharat (General Chairs APLAS-ATVA 2025) On behalf of APLAS-ATVA 2025 Organizing Committee ----- End forwarded message -----

2 months

1
0
0 0

RHPL@FSTTCS 2025: Deadline Extension

by abhisekh.sankaran＠tcs.com

============================================================= RHPL@FSTTCS 2025: Workshop on Research Highlights in Programming Languages December 2025, BITS Goa, co-located with FSTTCS 2025 Website: https://fmindia.cmi.ac.in/rhpl2025/ Submission link: https://forms.gle/RufuAs54zxsadp1n7 Extended submission deadline: October 3, 2025 IST ============================================================= Dear colleague, As you may know, FSTTCS 2025 (https://www.fsttcs.org.in/2025/) is going to be held at BITS Pilani, K K Birla Goa Campus (https://www.bits-pilani.ac.in/goa/) during December 17 – 19, 2025. The conference is organized by IARCS, the Indian Association for Research in Computing Science (https://www.iarcs.org.in/), in association with ACM India (https://india.acm.org/). It is a very visible forum for presenting original results in foundational aspects of Computer Science and Software Technology. As in the previous years, this year too, co-located with the main FSTTCS conference, IARCS is organizing the Workshop on Research Highlights in Programming Languages (RHPL@FSTTCS). The focus of the workshop will be on all areas of Programming Languages (PL), including but not limited to: - Applied formal methods - Automated and interactive theorem provers - Compilers - Concurrency and memory models - Domain and type theories - Program analysis and verification - Program sketching, synthesis and repair - Programming language design and semantics Further, in view of the increasing role of Artificial Intelligence (AI) and Machine Learning (ML) in PL theory and practice, the workshop also includes in its scope themes pertaining to the influences of AI/ML concepts and tools on the mentioned PL topics, and vice-versa; for instance, probabilistic programming languages. The website for the workshop is: https://fmindia.cmi.ac.in/rhpl2025/. The objective of RHPL is to foster interactions between the attendees of the workshop, and more broadly between researchers working on Programming Languages and the traditional FSTTCS community of researchers working on Theoretical Computer Science and Formal Methods. We solicit: (1) Talk proposals: On recent work that has been published in good venues, or is mature in terms of approach and evaluation. (2) Poster proposals: On early ideas that are promising but have not been developed fully. Selections of these proposals will be made based on the promise of research possibilities and their novelty. Proposals to the workshop can be based on one or more works, published or unpublished. They may be submitted using the Google form below. https://forms.gle/RufuAs54zxsadp1n7 The important dates for the workshop are as below. All dates are in Indian Standard Time (IST). - Submission portal opens: July 28, 2025 - Submission deadline: October 3, 2025 (earlier: September 18, 2025) - Notification: October 10, 2025 (earlier: September 25, 2025) - Early registration deadline: TBA - RHPL@FSTTCS: TBA We look forward to receiving your talk/poster proposals to the workshop. On behalf of the RHPL@FSTTCS workshop organizing committee: Abhisekh Sankaran (TCS Research) (co-Chair) Divyesh Unadkat (Synopsys) (co-Chair) Deepak D'Souza (IISc Bangalore) Uday Khedker (IIT Bombay) Kumar Madhukar (IIT Delhi) Kartik Nagar (IIT Madras) Sumanth Prabhu (TCS Research) Ganesan Ramalingam (Microsoft) Abhik Roychoudhury (National University of Singapore)

2 months, 1 week

1
0
0 0

CEFIPRA Project Research Associate Position

by Srinivas Pinisetty

*CEFIPRA Project Research Associate Position* CEFIPRA Research Associate (RA)/postdoc position for the *“**SINCRET: Scalable and incremental security monitoring and enforcement for timed systems**”* project. *Announcement:* Applications are invited for one Research Associate (RA)/postdoc position to work at IIT Bhubaneswar on the “*SINCRET: Scalable and incremental security monitoring and enforcement for timed systems*” project. It is a CEFIPRA Indo-French collaborative project under the DST-Inria targeted programme. Details of current members working on the project from IIT Bhubaneswar, India and form Inria, Rennes, France are available here: https://devine.inria.fr/SINCRET/People.htm *Background:* In recent years, research on monitoring runtime behaviour of a system has gained significant attention. The domain of Runtime Monitoring and Verification has gained popularity due to its focus on dynamic behaviour of the system. In a nutshell, Runtime Verification (RV) domain focuses on developing algorithms that automatically generates a monitor from a given specification. The monitor, then, captures the execution of the system and gives a verdict on whether it satisfies the given specification [1]. In 2000, Schneider [2] made the first significant attempt to define a class of security policies that are enforceable. This led to the advent of a new sub-domain of research called Runtime Enforcement (RE). RE can be thought of as an extension of the RV domain, that along with monitoring a system for a given specification, provides assurance that the system satisfies the specification [3, 4, 5]. We work in the field of runtime enforcement, with special focus on timed systems. We work towards developing compositional RE monitors for timed systems. *Objectives:* One of the primary objectives of the *SINCRET* project is to investigate and formulate the theory (and the corresponding monitor synthesis tools) related to incremental/compositionality of enforcers in the timed context. Compositionality refers to combining multiple individual enforcers effectively and efficiently. We will initially consider the enforcement monitor synthesis framework suitable for reactive Cyber Physical Systems (CPS) proposed in [8] for discrete timed properties. We will study/explore various schemes for incrementally adding/composing enforcers in such frameworks. We will consider various schemes for composing enforcers such as serial and parallel composition schemes. In addition to theory and the monitor synthesis tools, we will also explore pros/cons of these schemes using application scenarios related to security of CPSs. More details about the project like related literature, team members, recent publications etc. is available on the website: https://devine.inria.fr/SINCRET/index.html. *Vacant Position**:* The project currently has one vacant Research Associate (RA)/postdoc position. - *Eligibility*: PhD degree in computer science is preferred. However, candidates with masters’ in CSE with relevant research experience/publications are also welcome to apply. - *Remuneration*: It will be as per DST norms for a Research Associate (RA)/postdoc position. - *Location*: The work location is IIT Bhubaneswar, India. - *Preferred Knowledge, Skills & Abilities*: Background/knowledge in Formal Methods, Timed systems/Timed automata, programming and development skills, ability to work effectively in a team as well as independently, and good communication skills. *To apply and for queries about the position:* Those interested, to apply please send your CV to Dr. Srinivas Pinisetty (email: spinisetty(a)iitbbs.ac.in) before 30th September 2025. In case of any queries about the position, please contact Dr. Srinivas Pinisetty (email: spinisetty(a)iitbbs.ac.in). *References:* [1] Ezio Bartocci and Yli`es Falcone. Lectures on runtime verification. Springer, 2018. [2] Fred B Schneider. Enforceable security policies. ACM Transactions on Information and System Security (TISSEC), 3(1):30–50, 2000. [3] Jay Ligatti and Srikar Reddy. A theory of runtime enforcement, with results. In European Symposium on Research in Computer Security, pages 87–100. Springer, 2010. [4] Srinivas Pinisetty, Partha S Roop, Steven Smyth, Stavros Tripakis, and Reinhard von Hanxleden. Runtime enforcement of reactive systems using synchronous enforcers. In Proceedings of the 24th ACM SIGSOFT international SPIN symposium on model checking of software, pages 80–89, 2017. [5] Srinivas Pinisetty, Partha S Roop, Steven Smyth, Nathan Allen, Stavros Tripakis, and Reinhard Von Hanxleden. Runtime enforcement of cyber-physical systems. ACM Transactions on Embedded Computing Systems (TECS). ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Best Regards Dr. Srinivas Pinisetty Associate Professor (CSE) School of Electrical and Computer Sciences Indian Institute of Technology Bhubaneswar Odisha 752050, India https://www.iitbbs.ac.in/profile.php/srinivaspinisetty/

2 months, 2 weeks

1
0
0 0

IARCS Verification Seminar Series -- Talk by Soumyajit Paul on Sept. 16 at 1900 hrs IST

by VSS IARCS

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Soumyajit Paul, a post-doctoral researcher at the University of Liverpool. The talk is scheduled on Tuesday, September 16, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=M2EzajE4cT…> ). 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, Organizers, IARCS Verification Seminar Series ============================================================= Title: Resolving Nondeterminism by Chance Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. The notion of History Determinism (sometimes known as Good for Games) was introduced by Henzinger and Piterman in 2006 motivated by applications in reactive synthesis. Later, it has been studied for several models such as Pushdown systems, Timed automata, Vector Addition systems, etc. Motivated by checking qualitative properties in probabilistic verification, we introduce the setting where the resolver strategy can randomize and only needs to succeed with lower-bounded probability. In this talk, I will present our work on stochastic resolution of nondeterministic automata. I will discuss the expressiveness of stochastically-resolvable automata as well as our complexity results for deciding stochastic resolvability. In particular, we show that it is undecidable to check if a given NFA is stochastically resolvable with a given threshold. The problem however becomes decidable for the class of finitely-ambiguous automata. We also consider the related question of deciding whether an automata is resolvable with any positive threshold. We show that this problem is decidable for automata over unary alphabet as well as for finitely-ambiguous automata. I will present our complexity results for several well-studied classes of automata and also discuss natural extensions of some of these results to automata for omega regular languages. I will conclude with some interesting open questions. This is based on joint work with David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke and Di-de Yen. Bio: Soumyajit Paul is currently a post-doctoral researcher at University of Liverpool, working primarily with Sven Schewe. His research interests encompasses algorithmic game theory, probabilistic systems and formal methods. Earlier, he was a teaching and research fellow at Université Paris Cité, affiliated to IRIF. He did his PhD at LaBRI, Université de Bordeaux under the supervision of Hugo Gimbert and B. Srivathsan. His PhD research work focussed on the complexity of equilibrium computations in games where players may have imperfect information. Prior to his PhD, he completed his undergraduate and master's studies at Chennai Mathematical Institute.

2 months, 2 weeks

1
0
0 0

IARCS Verification Seminar Series -- Talk by Soumyajit Paul on Sept. 16 at 1900 hrs IST

by VSS IARCS

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Soumyajit Paul, a post-doctoral researcher at the University of Liverpool. The talk is scheduled on Tuesday, September 16, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=M2EzajE4cT…> ). 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, Organizers, IARCS Verification Seminar Series ============================================================= Title: Resolving Nondeterminism by Chance Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. The notion of History Determinism (sometimes known as Good for Games) was introduced by Henzinger and Piterman in 2006 motivated by applications in reactive synthesis. Later, it has been studied for several models such as Pushdown systems, Timed automata, Vector Addition systems, etc. Motivated by checking qualitative properties in probabilistic verification, we introduce the setting where the resolver strategy can randomize and only needs to succeed with lower-bounded probability. In this talk, I will present our work on stochastic resolution of nondeterministic automata. I will discuss the expressiveness of stochastically-resolvable automata as well as our complexity results for deciding stochastic resolvability. In particular, we show that it is undecidable to check if a given NFA is stochastically resolvable with a given threshold. The problem however becomes decidable for the class of finitely-ambiguous automata. We also consider the related question of deciding whether an automata is resolvable with any positive threshold. We show that this problem is decidable for automata over unary alphabet as well as for finitely-ambiguous automata. I will present our complexity results for several well-studied classes of automata and also discuss natural extensions of some of these results to automata for omega regular languages. I will conclude with some interesting open questions. This is based on joint work with David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke and Di-de Yen. Bio: Soumyajit Paul is currently a post-doctoral researcher at University of Liverpool, working primarily with Sven Schewe. His research interests encompasses algorithmic game theory, probabilistic systems and formal methods. Earlier, he was a teaching and research fellow at Université Paris Cité, affiliated to IRIF. He did his PhD at LaBRI, Université de Bordeaux under the supervision of Hugo Gimbert and B. Srivathsan. His PhD research work focussed on the complexity of equilibrium computations in games where players may have imperfect information. Prior to his PhD, he completed his undergraduate and master's studies at Chennai Mathematical Institute.

2 months, 2 weeks

1
0
0 0

RHPL@FSTTCS 2025: Third Call for Talk and Poster Proposals | Deadline: September 18

by abhisekh.sankaran＠tcs.com

============================================================= RHPL@FSTTCS 2025: Workshop on Research Highlights in Programming Languages December 2025, BITS Goa, co-located with FSTTCS 2025 Website: https://fmindia.cmi.ac.in/rhpl2025/ Submission link: https://forms.gle/RufuAs54zxsadp1n7 Submission deadline: September 18, 2025 IST ============================================================= Dear colleague, As you may know, FSTTCS 2025 (https://www.fsttcs.org.in/2025/) is going to be held at BITS Pilani, K K Birla Goa Campus (https://www.bits-pilani.ac.in/goa/) during December 17 – 19, 2025. The conference is organized by IARCS, the Indian Association for Research in Computing Science (https://www.iarcs.org.in/), in association with ACM India (https://india.acm.org/). It is a very visible forum for presenting original results in foundational aspects of Computer Science and Software Technology. As in the previous years, this year too, co-located with the main FSTTCS conference, IARCS is organizing the Workshop on Research Highlights in Programming Languages (RHPL@FSTTCS). The focus of the workshop will be on all areas of Programming Languages (PL), including but not limited to: - Applied formal methods - Automated and interactive theorem provers - Compilers - Concurrency and memory models - Domain and type theories - Program analysis and verification - Program sketching, synthesis and repair - Programming language design and semantics Further, in view of the increasing role of Artificial Intelligence (AI) and Machine Learning (ML) in PL theory and practice, the workshop also includes in its scope themes pertaining to the influences of AI/ML concepts and tools on the mentioned PL topics, and vice-versa; for instance, probabilistic programming languages. The website for the workshop is: https://fmindia.cmi.ac.in/rhpl2025/. The objective of RHPL is to foster interactions between the attendees of the workshop, and more broadly between researchers working on Programming Languages and the traditional FSTTCS community of researchers working on Theoretical Computer Science and Formal Methods. We solicit: (1) Talk proposals: On recent work that has been published in good venues, or is mature in terms of approach and evaluation. (2) Poster proposals: On early ideas that are promising but have not been developed fully. Selections of these proposals will be made based on the promise of research possibilities and their novelty. Proposals to the workshop can be based on one or more works, published or unpublished. They may be submitted using the Google form below. https://forms.gle/RufuAs54zxsadp1n7 The important dates for the workshop are as below. All dates are in Indian Standard Time (IST). - Submission portal opens: July 28, 2025 - Submission deadline: September 18, 2025 - Notification: September 25, 2025 - Early registration deadline: TBA - RHPL@FSTTCS: TBA We look forward to receiving your talk/poster proposals to the workshop. On behalf of the RHPL@FSTTCS workshop organizing committee: Abhisekh Sankaran (TCS Research) (co-Chair) Divyesh Unadkat (Synopsys) (co-Chair) Deepak D'Souza (IISc Bangalore) Uday Khedker (IIT Bombay) Kumar Madhukar (IIT Delhi) Kartik Nagar (IIT Madras) Sumanth Prabhu (TCS Research) Ganesan Ramalingam (Microsoft) Abhik Roychoudhury (National University of Singapore)

2 months, 2 weeks

1
0
0 0

MMAC Workshop (co-located with ATVA 2025): Call for participation and poster submission

by VSS IARCS

Dear all, We invite you to participate in MMAC 2025 (https://mmautomata.github.io/) — a post-conference of ATVA 2025 (https://conf.researchr.org/home/atva-2025) on Milestones and Motifs in Automata and Concurrency. This workshop is going to be held at IIIT Bangalore, on October 31, 2025. The registration for the workshop is open; the early bird registration deadline ends on September 30th. Here is the link to register: https://conf.researchr.org/attending/atva-2025/registration MMAC 2025 will also host a Poster Session ( https://mmautomata.github.io/#poster) -- a forum for students, faculty and industry practitioners working in the broad area of automated analysis, synthesis, and verification of hardware and software systems, including but not limited to automata, concurrency and timed systems, to present their research work to the workshop attendees. Early-stage ideas are more than welcome. We anticipate it to be an excellent opportunity to get feedback, and network with peers and experts in the field. Note that there will be no proceedings for this workshop and thus the shortlisted posters would not be a part of any formal proceedings. If you are interested in presenting a poster, please submit an entry using this Google form (https://forms.gle/r2WiAHVQWtX7s1v39). The submission deadline is September 25th. Shortlisted entries will be notified by September 28th. The poster presentation would only be an in-person event; an author of every shortlisted poster would be expected to register for MMAC 2025 (https://conf.researchr.org/attending/atva-2025/registration) and present the poster at the workshop. We look forward to your participation. Needless to say, we'd be very happy to clarify any questions you might have in this regard. If you have any queries, please write to the organisers at mmautomata2025(a)gmail.com. Best regards, C. Aiswarya (Chennai Mathematical Institute) S. Akshay (IIT Bombay) Kumar Madhukar (IIT Delhi)

2 months, 3 weeks

1
0
0 0

2025

2024

2023

2022

FMIndia September 2025