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-…
Important Dates
Submissions Deadline: August 31, 2025
Review result notification: November 1, 2025
Acceptance/rejection: December 31, 2025
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
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/
Call for Papers
International Workshop on Petri Nets and Software Engineering
PNSE’25, Paris, France, June 23-24, 2025
http://www.pnse.de
PNSE’25 is a satellite event of PETRI NETS’25
https://petrinets25.github.io/web/
Scope
For the successful realisation of complex systems of interacting and
reactive software and hardware components the use of a precise language at
different stages of the development process is of crucial importance.
Petri nets are becoming increasingly popular in this area, as they provide
a uniform language supporting the tasks of modelling, validation, and
verification.
We welcome contributions describing original research in topics related to
Petri nets in combination with software engineering, addressing open
problems
or presenting new ideas regarding the relation of Petri nets and software
engineering. Furthermore, we look for surveys addressing open problems
and new
applications of Petri nets and for Petri nets.
Important Dates:
Deadline for papers: 25 April 2025
Notification of paper acceptance: 19 May 2025
Deadline for posters: 25 May 2025
Notification of poster acceptance: 28 May 2025
Deadline for final revisions: 30 May 2025
Topics
Topics of interest include (but are not limited to):
- Software Engineering
agile development
product lines
software in business contexts
software development and production environments; DevOps; IDEs;
continuous integration
programming and concurrency
technologies: hadoop / MapReduce; akka, Spark; Flink; STORM etc.
distributed database technology: redis; cassandra; CouchDB; mongoDB etc.
concepts for mobility, concurrency, non-determinism, distribution,
embedding, flexibility
social concepts for norms, rules, contracts, communication,
co-ordination, co-operation
software engineering addressing Petri nets, UML techniques, BPMN, BPEL,
eEPCs, CMMN and other modelling techniques
- Modelling
representation of formal models by intuitive modelling concepts
guidelines for the construction of system models
adaption, integration, and enhancement of concepts from other disciplines
views and abstractions of systems
meta-modelling and domain specific languages (DSLs)
model-driven architecture
modelling software landscapes
web service-based software development
- Validation and Execution
prototyping
simulation, observation, animation
code generation and execution
testing and debugging
efficient implementation
- Verification
structural methods (e.g. place invariants, reduction rules)
results for structural subclasses of nets
state space based approaches
efficient model checking
assertional and deductive methods (e.g. temporal logics)
process algebraic methods
model and graph transformation
applications of category theory, rewriting logic and linear logic
- Application of Petri nets and Software Engineering, in particular in
the domains of …
education, training and teaching at any level,
flexible manufacturing,
logistics,
telecommunication,
big data,
cyber-physical systems,
internet-of-things,
grid and cloud computing,
distributed systems,
workflow management and
embedded systems.
- Tools in the fields mentioned above
Submissions
The program committee invites submissions of full contributions (up to
20 pages excluding references) or short contributions (5 - 8 pages
excluding references). Ongoing work (up to 3 pages including references)
can be presented in a special poster session.
Papers must be submitted in electronic form (PDF) using the CEUR latex
style:
http://ceur-ws.org/Vol-XXX/CEURART.zip
Submissions should include title, authors' addresses, E-mail addresses,
keywords and an abstract. For your submission please use the track
"International Workshop on Petri Nets and Software Engineering 2025" at:
https://easychair.org/conferences/?conf=petrinets2025
The papers will be peer reviewed. Accepted contributions will be
included in the workshop proceedings, which will be available at the
workshop and published online.
The best papers from the workshop will be invited for publication in a
volume of the journal sub-line of Lecture Notes in Computer Science
entitled "Transactions on Petri Nets and Other Models of Concurrency"
(ToPNoC). The papers are expected to be thoroughly revised and they will
go through a totally new round of reviewing.
PC Chairs
Michael Köhler-Bußmeier, University of Applied Science Hamburg, Germany
Daniel Moldt, University of Hamburg, Germany
Heiko Rölke, FH Graubünden, Austria
In case of any problems please contact us by email: pnse25(a)easychair.org
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: August 31, 2025
Review result notification: November 1, 2025
Acceptance/rejection: December 31, 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/
================================================================================
Formal Methods in Computer-Aided Design (FMCAD) 2025 - Deadline Extension
================================================================================
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 28, 2025 (extended from April 20, 2025)
*Paper Submission Deadline: May 5, 2025 (extended from 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 Hyvärinen, 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 University 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
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: August 31, 2025
Review result notification: November 1, 2025
Acceptance/rejection: December 31, 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/
Call for Papers - Deadlines extended
-------------------------------
**Paper submission extended to April 25, 2025 (AoE)**
The 23rd International Symposium on Automated Technology for
Verification and Analysis (ATVA 2025)
27-30 October 2025,
Bangalore, India
https://conf.researchr.org/home/atva-2025
AIM AND SCOPE
ATVA 2025 is the 23rd in a series of symposia aimed at bringing together
academics, industrial researchers and practitioners in the area of
theoretical and practical aspects of automated analysis, synthesis, and
verification of hardware and software systems. ATVA solicits high
quality submissions in the following suggestive list of topics:
- Formalisms for modeling hardware, software and embedded systems
- Specification and verification of finite-state, infinite-state and
parameterized systems
- Program analysis and software verification
- Analysis and verification of hardware circuits, systems-on-chip
and embedded systems
- Analysis of real-time, hybrid, priced, weighted and probabilistic
systems
- Deductive, algorithmic, compositional, and abstraction/refinement
techniques for analysis and verification
- Analytical techniques for safety, security, and dependability
- Testing and runtime analysis based on verification technology
- Analysis and verification of parallel and concurrent systems
- Verification in industrial practice
- Synthesis for hardware and software systems
- Applications and case studies of verification
- Automated tool support for verification
- Testing and verification of neural networks
- Testing and verification of autonomous systems
IMPORTANT DATES (all deadlines in AoE)
- Abstract + Paper submission deadline: April 25, 2025
- Author response period: June 17 - 20, 2025
- Paper notification: July 4, 2025
- Camera-ready deadline: August 1, 2025
- Tutorials: October 27, 2025
- Workshops: 31 October 2025
- Conference: October 28 - October 30, 2025
ARTIFACT SUBMISSION DEADLINES (all deadlines in AoE):
For tool papers:
- Artifact submission deadline: May 2, 2025
- Smoke test reviews: May 9, 2025
- Submission of revised artifacts: May 11, 2025
- Author notification: July 4, 2025
For accepted regular papers:
- Artifact submission: July 8, 2025
- Author notification: July 27, 2025
SUBMISSION GUIDELINES
ATVA welcomes submissions in the following two categories:
- Regular research papers (18 pages, excluding references, must be
anonymized)
- Tool papers (10 pages, excluding references, not anonymized)
Submissions authored or co-authored by members of the program committee
are allowed and encouraged.
Papers must be submitted through
EasyChair<https://easychair.org/conferences/?conf=atva2025>.
Submissions in both categories must be in Springer's LNCS format.
Accepted papers in both categories will be published in Springer's
Lecture Notes in Computer Science series. A few outstanding papers will
be selected for a distinguished paper award. At least one author of each
accepted paper is expected to register and present the paper at the
conference.
REGULAR PAPERS
Regular papers should not exceed 18 pages in Springer’s LNCS format, not
counting references and appendices. Additional material may be placed in
an appendix, to be read at the discretion of the reviewers, and to be
omitted in the final version.
Regular papers at ATVA 2025 will follow a full *double-blind* review
process, which means that author names and affiliations must be omitted
from the submission. Additionally, if a submission refers to prior work
done by the authors, the reference should be made in the third person.
These are firm submission requirements, and any regular paper that does
not conform to these requirements will be rejected without review.
Authors of accepted regular papers will be invited (but are not
required) to submit a relevant artifact for evaluation by the artifact
evaluation committee. The submission deadline for this artifact
evaluation will be soon after the paper acceptance notification.
Independent of the artifact evaluation process, research paper authors
are encouraged to include a URL to a repository in their original
submission, if such a repository is available and is pertinent to the
paper. This repository could contain code, datasets, results, etc. This
would be for the consideration of the PC reviewers of the submission, at
their discretion. If such a URL is included in the submission, the
contents of the repository should adhere to the guidelines of a
double-blind review process. The review process will include a rebuttal
period where the authors will have the option to respond to reviewer
comments. An artifact evaluation will be undertaken, which will be
optional for regular papers and mandatory for tool papers.
TOOL PAPERS
Tool papers should not exceed 10 pages in Springer’s LNCS format, not
counting references. Tool papers will follow a single-blind review
process. They do NOT need to be anonymized. Tool paper submissions MUST
include a URL to an archival site from where the tool can be downloaded
or accessed online for evaluation by the artifact evaluation committee.
The site must also contain a set of examples, and a user manual that
describes usage of the tool through examples. If the tool needs to be
downloaded and installed, the site must contain instructions for
installing the tool on Linux, Windows or MacOS. Packing the artifact as
a Docker container is recommended. Papers describing tools that have
already been presented (in any conference) will be accepted only if
significant and clear enhancements to the tool are reported and
implemented.
Acceptance of tool paper submissions is contingent on successful
artifact evaluation at the “functional” level. In special cases, where
an artifact cannot be submitted, the authors should contact the Artifact
Evaluation chairs to find alternate modes of artifact evaluation. More
details about artifact evaluation can be found on the conference web site.
CALL FOR WORKSHOPS
We invite proposals for organizing workshops as part of ATVA 2025.
Workshops will be held post-conference, on 31 October 2025. Proposals
may be submitted via this Proposal
Form<https://docs.google.com/forms/d/e/1FAIpQLSfyZ7otNMqivg5xnS2aPIyzEKW__LPC2SE…>.
The last date for submitting workshop proposals is 30 April 2025.
CALL FOR TUTORIALS
We invite proposals for organizing tutorials as a part of ATVA 2025.
Tutorials will be held pre-conference, on 27 October 2025. Tutorial
proposals can be submitted via this Proposal
Form<https://docs.google.com/forms/d/e/1FAIpQLSeLRNufBv7sL-_SJWJXhs7aLOnML_mn3S9…>.
The last date for submitting tutorial proposals is 30 April 2025.
GENERAL CHAIR
Deepak D’Souza, Indian Institute of Science, Bangalore, India
LOCAL ORGANIZATION CHAIR
Sujit Kumar Chakrabarti, IIIT-Bangalore, India
PROGRAM CHAIRS
Meenakshi D’Souza, IIIT-Bangalore, India < meenakshi(a)iiitb.ac.in >
K. V. Raghavan, Indian Institute of Science, Bangalore, India <
raghavan(a)iisc.ac.in >
B. Srivathsan, Chennai Mathematical Institute, Chennai, India <
sri(a)cmi.ac.in >
ARTIFACT EVALUATION CHAIRS
Jie An, Institute of Software, Chinese Academy of Sciences, Beijing, China
Priyanka Golia, IIT Delhi, India
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.
A reminder about this talk tomorrow. The Europe times in the original message were wrong. They have been corrected below.
----- 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 New York, 1400 GMT, 1600 Amsterdam, 1930 Bangalore, 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, 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 -----
----- Forwarded message from Meenakshi D'Souza <meenakshi(a)iiitb.ac.in> -----
From: Meenakshi D'Souza <meenakshi(a)iiitb.ac.in>
Date: Sat, 5 Apr 2025 18:03:40 +0000
Subject: ATVA 2025: Joint Call for Papers, Workshops and Tutorials
Call for Papers, Workshops and Tutorials
-------------------------------------------------------
The 23rd International Symposium on Automated Technology for Verification and Analysis (ATVA 2025)
27-30 October 2025,
Bangalore, India
https://conf.researchr.org/home/atva-2025
AIM AND SCOPE
ATVA 2025 is the 23rd in a series of symposia aimed at bringing together academics, industrial researchers and practitioners in the area of theoretical and practical aspects of automated analysis, synthesis, and verification of hardware and software systems. ATVA solicits high quality submissions in the following suggestive list of topics:
- Formalisms for modeling hardware, software and embedded systems
- Specification and verification of finite-state, infinite-state and parameterized systems
- Program analysis and software verification
- Analysis and verification of hardware circuits, systems-on-chip and embedded systems
- Analysis of real-time, hybrid, priced, weighted and probabilistic systems
- Deductive, algorithmic, compositional, and abstraction/refinement techniques for analysis and verification
- Analytical techniques for safety, security, and dependability
- Testing and runtime analysis based on verification technology
- Analysis and verification of parallel and concurrent systems
- Verification in industrial practice
- Synthesis for hardware and software systems
- Applications and case studies of verification
- Automated tool support for verification
- Testing and verification of neural networks
- Testing and verification of autonomous systems
IMPORTANT DATES (all deadlines in AoE)
- Abstract submission deadline: April 11, 2025
- Paper submission deadline: April 18, 2025
- Author response period: June 10 - 13, 2025
- Paper notification: June 25, 2025
- Camera-ready deadline: July 25, 2025
- Tutorials: October 27, 2025
- Workshops: 31 October 2025
- Conference: October 28 - October 30, 2025
ARTIFACT SUBMISSION DEADLINES (all deadlines in AoE):
For tool papers:
- Artifact submission deadline: April 25, 2025
- Smoke test reviews: May 1, 2025
- Submission of revised artifacts: May 3, 2025
- Author notification: June 25, 2025
For accepted regular papers:
- Artifact submission: June 28, 2025
- Author notification: July 21, 2025
SUBMISSION GUIDELINES
ATVA welcomes submissions in the following two categories:
- Regular research papers (18 pages, excluding references, must be anonymized)
- Tool papers (10 pages, excluding references, not anonymized)
Submissions authored or co-authored by members of the program committee are allowed and encouraged.
Papers must be submitted through EasyChair<https://easychair.org/conferences/?conf=atva2025>.
Submissions in both categories must be in Springer's LNCS format. Accepted papers in both categories will be published in Springer's Lecture Notes in Computer Science series. A few outstanding papers will be selected for a distinguished paper award. At least one author of each accepted paper is expected to register and present the paper at the conference.
REGULAR PAPERS
Regular papers should not exceed 18 pages in Springer’s LNCS format, not counting references and appendices. Additional material may be placed in an appendix, to be read at the discretion of the reviewers, and to be omitted in the final version.
Regular papers at ATVA 2025 will follow a full *double-blind* review process, which means that author names and affiliations must be omitted from the submission. Additionally, if a submission refers to prior work done by the authors, the reference should be made in the third person. These are firm submission requirements, and any regular paper that does not conform to these requirements will be rejected without review.
Authors of accepted regular papers will be invited (but are not required) to submit a relevant artifact for evaluation by the artifact evaluation committee. The submission deadline for this artifact evaluation will be soon after the paper acceptance notification. Independent of the artifact evaluation process, research paper authors are encouraged to include a URL to a repository in their original submission, if such a repository is available and is pertinent to the paper. This repository could contain code, datasets, results, etc. This would be for the consideration of the PC reviewers of the submission, at their discretion. If such a URL is included in the submission, the contents of the repository should adhere to the guidelines of a double-blind review process. The review process will include a rebuttal period where the authors will have the option to respond to reviewer comments. An artifact evaluation will be undertaken, which will be optional for regular papers and mandatory for tool papers.
TOOL PAPERS
Tool papers should not exceed 10 pages in Springer’s LNCS format, not counting references. Tool papers will follow a single-blind review process. They do NOT need to be anonymized. Tool paper submissions MUST include a URL to an archival site from where the tool can be downloaded or accessed online for evaluation by the artifact evaluation committee. The site must also contain a set of examples, and a user manual that describes usage of the tool through examples. If the tool needs to be downloaded and installed, the site must contain instructions for installing the tool on Linux, Windows or MacOS. Packing the artifact as a Docker container is recommended. Papers describing tools that have already been presented (in any conference) will be accepted only if significant and clear enhancements to the tool are reported and implemented.
Acceptance of tool paper submissions is contingent on successful artifact evaluation at the “functional” level. In special cases, where an artifact cannot be submitted, the authors should contact the Artifact Evaluation chairs to find alternate modes of artifact evaluation. More details about artifact evaluation can be found on the conference web site.
CALL FOR WORKSHOPS
We invite proposals for organizing workshops as part of ATVA 2025. Workshops will be held post-conference, on 31 October 2025. Proposals may be submitted via this Proposal Form<https://docs.google.com/forms/d/e/1FAIpQLSfyZ7otNMqivg5xnS2aPIyzEKW__LPC2SE…>.
The last date for submitting workshop proposals is 30 April 2025.
CALL FOR TUTORIALS
We invite proposals for organizing tutorials as a part of ATVA 2025. Tutorials will be held pre-conference, on 27 October 2025. Tutorial proposals can be submitted via this Proposal Form<https://docs.google.com/forms/d/e/1FAIpQLSeLRNufBv7sL-_SJWJXhs7aLOnML_mn3S9…>.
The last date for submitting tutorial proposals is 30 April 2025.
GENERAL CHAIR
Deepak D’Souza, Indian Institute of Science, Bangalore, India
LOCAL ORGANIZATION CHAIR
Sujit Kumar Chakrabarti, IIIT-Bangalore, India
PROGRAM CHAIRS
Meenakshi D’Souza, IIIT-Bangalore, India < meenakshi(a)iiitb.ac.in >
K. V. Raghavan, Indian Institute of Science, Bangalore, India < raghavan(a)iisc.ac.in >
B. Srivathsan, Chennai Mathematical Institute, Chennai, India < sri(a)cmi.ac.in >
ARTIFACT EVALUATION CHAIRS
Jie An, Institute of Software, Chinese Academy of Sciences, Beijing, China
Priyanka Golia, IIT Delhi, India
----- End forwarded message -----
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.
