FYI
---------- Forwarded message ---------
From: Nija Shi <nija.nfm24(a)gmail.com>
Date: Thu, 28 Sept 2023 at 19:48
Subject: CFP: NASA Formal Methods Symposium 2024
To: Undisclosed Recipients <nija.nfm24(a)gmail.com>
The NASA Formal Methods community invites you to submit a paper to:
The 16th NASA Formal Methods Symposium (NFM 2024)
June 4-6, 2024
Moffett Field, California
--------------------------------------------------
Important Dates:
--------------------------------------------------
Abstract submission: December 1, 2023
Full paper submission: December 8, 2023
Notification: February 16, 2024
Camera-ready version: March 15, 2024
--------------------------------------------------
Theme of the Symposium:
--------------------------------------------------
The widespread use and increasing complexity of mission-critical and
safety-critical systems at NASA and in the aerospace industry requires
advanced
technologies to address their specification, design, verification,
validation,
and certification processes. For example, there is an increasing need for
autonomous systems in deep space missions including NASA’s Moon to Mars
exploration plans. The NASA Formal Methods Symposium is a forum to foster
collaboration between theoreticians and practitioners from NASA, other
government agencies, academia, and industry, with the goal of identifying
challenges and providing solutions towards achieving assurance for such
critical systems. The focus of this symposium is on formal techniques for
software and system assurance for applications in space, aviation, robotics,
and other NASA-relevant safety-critical systems. This year’s symposium
extends
the focus to safety assurance of machine learning enabled autonomous
systems,
formal methods for digital transformation, and accessibility for new
industries.
--------------------------------------------------
Topics of Interest:
--------------------------------------------------
Advances in Formal Methods
* Formal verification, model checking, and static analysis
* Interactive and automated theorem proving
* Program and specification synthesis, code transformation and generation
* Run-time verification and test case generation
* Techniques and algorithms for scaling formal methods
* Design for verification and correct-by-design techniques
* Requirements generation, specification, and validation
Integration of Formal Methods
* Use of machine learning techniques in formal methods
* Integration of formal methods and software engineering
* Integration of diverse formal methods techniques
* Combination of formal methods with simulation and analysis techniques
Formal Methods in Practice
* Experience reports of application of formal methods in industry
* Use of formal methods in education
* Applications of formal methods in:
- concurrent and distributed systems
- fault-detection, diagnostics, and prognostics systems
- human-machine interaction analysis
Safety Assurance of Autonomous Systems
* Verification of machine learning (ML) enabled systems
* Runtime monitoring or model checking to ensure safe operation
* Formal specifications and modeling of ML enabled systems
* Case-studies/experience reports exploring the application of formal
methods
in autonomous safety-critical, cyber-physical and hybrid systems
* Using formal evidence for certification of ML enabled systems
Formal Methods for Digital Transformation
* Applications related to Digital Twin & Digital Thread
* Verification for integrated design and manufacturing
* AI digital assistants for system design
* Runtime monitoring for Smart Campus & Smart Cities
Accessibility of Formal Methods for New Industries
* "New Space" markets
* Advanced Air Mobility and Startup Aviation
* Formal Methods as a Service
--------------------------------------------------
Submissions:
--------------------------------------------------
There are two categories of submissions:
* Regular Papers (15 pages) including references, describing fully developed
work and complete results
* Short Papers (6 pages) including references, in one of the categories
below:
- Tool papers describing novel and publicly available tools
- Case studies detailing applications of formal methods
- New emerging ideas in the topics of interest
All papers should be in English and describe original work that has not been
published or submitted elsewhere. NFM24 will be a hybrid conference.
Authors of
accepted papers are encouraged to present their work in person at the
conference.
There will be a tool demonstration session at the conference, where tool
developers get to showcase their tools interactively with the attendees. All
tool papers, under the short papers category, are required to participate in
the tool demonstration session. Authors of regular papers are also welcome
to
participate in the tool demonstration session to showcase their application.
All submitters who are interested in participating in the tool demonstration
session must include an additional appendix (maximum 4 pages and will not
appear in the proceedings) containing the description of the proposed demo
and
the URL to a screencast demonstrating the tool. Authors of all accepted
papers
additionally have an opportunity to present a poster.
All submissions will be fully reviewed by members of the Program Committee.
Accepted regular and short papers will be published in the Formal Methods
subline of Springer’s Lecture Notes in Computer Science (LNCS) and must use
LNCS style formatting described on
https://www.springer.com/gp/computer-science/lncs/conference-proceedings-gu…
.
Papers must be submitted in PDF format at the EasyChair submission site,
https://easychair.org/conferences/?conf=nfm2024.
--------------------------------------------------
Location and Cost:
--------------------------------------------------
The symposium will take place at the NASA Ames Conference Center,
Moffett Field, California, USA.
There will be no registration fee charged to participants. All
interested individuals, including non-US citizens, are welcome to
attend, listen to the talks, and participate in discussions. However,
all attendees must register.
Nathan Benz
Divya Gopinath
Nija Shi
NFM '24 Chairs
nfm24-chairs(a)lists.nasa.gov
FYI
---------- Forwarded message ---------
From: Shi, Nija (ARC-TI) <nija.shi(a)nasa.gov>
Date: Thu, 21 Sept 2023 at 08:56
Subject: [SEWORLD] CFP: NASA Formal Methods Symposium 2024
To: SEWORLD(a)SIGSOFT.ORG <SEWORLD(a)sigsoft.org>
The NASA Formal Methods community invites you to submit a paper to:
The 16th NASA Formal Methods Symposium (NFM 2024)
June 4-6, 2024
Moffett Field, California
--------------------------------------------------
Important Dates:
--------------------------------------------------
Abstract submission: December 1, 2023
Full paper submission: December 8, 2023
Notification: February 16, 2024
Camera-ready version: March 15, 2024
--------------------------------------------------
Theme of the Symposium:
--------------------------------------------------
The widespread use and increasing complexity of mission-critical and
safety-critical systems at NASA and in the aerospace industry requires
advanced
technologies to address their specification, design, verification,
validation,
and certification processes. For example, there is an increasing need for
autonomous systems in deep space missions including NASA’s Moon to Mars
exploration plans. The NASA Formal Methods Symposium is a forum to foster
collaboration between theoreticians and practitioners from NASA, other
government agencies, academia, and industry, with the goal of identifying
challenges and providing solutions towards achieving assurance for such
critical systems. The focus of this symposium is on formal techniques for
software and system assurance for applications in space, aviation,
robotics,
and other NASA-relevant safety-critical systems. This year’s symposium
extends
the focus to safety assurance of machine learning enabled autonomous
systems,
formal methods for digital transformation, and accessibility for new
industries.
--------------------------------------------------
Topics of Interest:
--------------------------------------------------
Advances in Formal Methods
* Formal verification, model checking, and static analysis
* Interactive and automated theorem proving
* Program and specification synthesis, code transformation and generation
* Run-time verification and test case generation
* Techniques and algorithms for scaling formal methods
* Design for verification and correct-by-design techniques
* Requirements generation, specification, and validation
Integration of Formal Methods
* Use of machine learning techniques in formal methods
* Integration of formal methods and software engineering
* Integration of diverse formal methods techniques
* Combination of formal methods with simulation and analysis techniques
Formal Methods in Practice
* Experience reports of application of formal methods in industry
* Use of formal methods in education
* Applications of formal methods in:
- concurrent and distributed systems
- fault-detection, diagnostics, and prognostics systems
- human-machine interaction analysis
Safety Assurance of Autonomous Systems
* Verification of machine learning (ML) enabled systems
* Runtime monitoring or model checking to ensure safe operation
* Formal specifications and modeling of ML enabled systems
* Case-studies/experience reports exploring the application of formal
methods
in autonomous safety-critical, cyber-physical and hybrid systems
* Using formal evidence for certification of ML enabled systems
Formal Methods for Digital Transformation
* Applications related to Digital Twin & Digital Thread
* Verification for integrated design and manufacturing
* AI digital assistants for system design
* Runtime monitoring for Smart Campus & Smart Cities
Accessibility of Formal Methods for New Industries
* "New Space" markets
* Advanced Air Mobility and Startup Aviation
* Formal Methods as a Service
--------------------------------------------------
Submissions:
--------------------------------------------------
There are two categories of submissions:
* Regular Papers (15 pages) including references, describing fully
developed
work and complete results
* Short Papers (6 pages) including references, in one of the categories
below:
- Tool papers describing novel and publicly available tools
- Case studies detailing applications of formal methods
- New emerging ideas in the topics of interest
All papers should be in English and describe original work that has not
been
published or submitted elsewhere. NFM24 will be a hybrid conference.
Authors of
accepted papers are encouraged to present their work in person at the
conference.
There will be a tool demonstration session at the conference, where tool
developers get to showcase their tools interactively with the attendees.
All
tool papers, under the short papers category, are required to participate
in
the tool demonstration session. Authors of regular papers are also welcome
to
participate in the tool demonstration session to showcase their
application.
All submitters who are interested in participating in the tool
demonstration
session must include an additional appendix (maximum 4 pages and will not
appear in the proceedings) containing the description of the proposed demo
and
the URL to a screencast demonstrating the tool. Authors of all accepted
papers
additionally have an opportunity to present a poster.
All submissions will be fully reviewed by members of the Program Committee.
Accepted regular and short papers will be published in the Formal Methods
subline of Springer’s Lecture Notes in Computer Science (LNCS) and must use
LNCS style formatting described on
https://www.springer.com/gp/computer-science/lncs/conference-proceedings-gu….
Papers must be submitted in PDF format at the EasyChair submission site,
https://easychair.org/conferences/?conf=nfm2024.
--------------------------------------------------
Location and Cost:
--------------------------------------------------
The symposium will take place at the NASA Ames Conference Center,
Moffett Field, California, USA.
There will be no registration fee charged to participants. All
interested individuals, including non-US citizens, are welcome to
attend, listen to the talks, and participate in discussions. However,
all attendees must register.
Nathan Benz
Divya Gopinath
Nija Shi
NFM '24 Chairs
nfm24-chairs(a)lists.nasa.gov
============================================================
To contribute to SEWORLD, send your submission to
mailto:seworld@sigsoft.org
http://sigsoft.org/resources/seworld.html provides more
information on SEWORLD as well as links to a complete
archive of messages posted to the list.
============================================================
FYI
---------- Forwarded message ---------
From: Arie Gurfinkel <arie.gurfinkel(a)uwaterloo.ca>
Date: Fri, Sep 15, 2023, 05:09
Subject: CAV 2024 -- First Call for Papers
To: Arie Gurfinkel <arie.gurfinkel(a)uwaterloo.ca>
CAV 2024: 36th International Conference on Computer-Aided Verification July
22-27 2024, Montreal, Canada
*CALL FOR PAPERS*
http://i-cav.org/2024/call-for-papers/
*IMPORTANT DATES*
All deadlines are AoE (Anywhere on Earth)
Paper submission: January 19, 2024
Rebuttal period: February 29 – March 3, 2024
Author notification: March 26, 2024
Artifact submission: April 8, 2024 (mandatory for tool papers)
Artifact notification: May 10, 2024
Final version due: May 19, 2024
Workshops: July 22-23, 2024
Main Conference: July 24-27, 2024
*CAV AWARD*
Nomination deadline: March 1, 2024
Submission site
Main submission site is https://easychair.org/conferences/?conf=cav2024
*SCOPE*
CAV 2024 is the 36th in a series dedicated to the advancement of the theory
and practice of computer-aided formal analysis methods for hardware and
software systems. The conference covers the spectrum from theoretical
results to concrete applications, with an emphasis on practical
verification tools and the algorithms and techniques that are needed for
their implementation. CAV considers it vital to continue spurring advances
in hardware and software verification while expanding to new domains such
as machine learning, autonomous systems, and computer security. The
proceedings of the conference will be published in the Springer-Verlag
Lecture Notes in Computer Science series. A selection of papers is expected
to be invited to a special issue of Formal Methods in System Design and the
Journal of the ACM.
Topics of interest include but are not limited to:
- Algorithms and tools for verifying models and implementations
- Algorithms and tools for system synthesis
- Algorithms and tools that combine verification and learning
- Mathematical and logical foundations of verification and synthesis
- Specifications and correctness criteria for programs and systems
- Deductive verification using proof assistants
- Hardware verification techniques
- Program analysis and software verification
- Software synthesis
- Hybrid systems and embedded systems verification
- Formal methods for cyber-physical systems
- Compositional and abstraction-based techniques for verification
- Probabilistic and statistical approaches to verification
- Verification methods for parallel and concurrent systems
- Testing and run-time analysis based on verification technology
- Decision procedures and solvers for verification and synthesis
- Applications and case studies in verification and synthesis
- Verification in industrial practice
- New application areas for algorithmic verification and synthesis
- Formal models and methods for security
- Formal models and methods for biological systems
Submissions on a wide range of topics are sought, particularly ones that
identify new research directions. CAV 2024 is not limited to topics
discussed in previous instances of the conference. Authors concerned about
the appropriateness of a topic may communicate with the conference chairs
prior to submission.
*CAV AWARD*
The CAV award is given annually at the CAV conference for fundamental
contributions to the field of Computer-Aided Verification.
CAV Award Nomination deadline: March 1st, 2024
Nominations should include a proposed citation (up to 25 words), a succinct
(100-250 words) description of the contribution(s), and a detailed
statement to justify the nomination. The cited contribution(s) must have
been made not more recently than five years ago and not over twenty five
years ago. In addition, the contribution(s) should not yet have received
recognition via a major award, such as the ACM Turing or Kanellakis Awards.
The nominee may have received such an award for other contributions.
For previous winners of the award, please see the main CAV award page (
http://i-cav.org/cav-award/).
Nominations should be submitted by e-mail to a member of the committee. For
details, please see http://i-cav.org/2024/cav-award/.
*PAPER SUBMISSION*
Paper submissions in CAV fall into one of the following three categories
(see more information below):
- Regular Papers (18 pages max, must be anonymized)
- Tool Papers (10 pages max, not anonymized)
- Industrial Experience Reports & Case Studies. (10 pages max, not
anonymized)
Papers in all three categories must be submitted by January 19th, 2024 AoE,
and should be in LNCS format. Simultaneous submission to other conferences
with proceedings or submission of material that has already been published
elsewhere is not allowed. The review process will include a
feedback/rebuttal period where authors will have the option to respond to
reviewer comments. The PC chairs may solicit further reviews after the
rebuttal period.
*REGULAR PAPERS*
Regular papers should not exceed 18 pages in LNCS format, not counting
references and appendices.
Regular papers at CAV 2024 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.
We do not discourage authors to put their submission on arXiv, but we
strongly encourage authors to not put the work on arXiv around (within 1
week) or shortly after (within 1 month) the submission deadline, because
potential reviewers may be subscribed to receive updates on recently posted
papers.
Authors can include a clearly marked appendix at the end of their
submissions that is exempt from the page limit restrictions. However, the
reviewers are not obliged to read the contents of these appendices. Regular
papers should contain original research and sufficient detail to assess the
merits and relevance of the contribution. Papers will be evaluated on the
basis of a combination of correctness, technical depth, significance,
novelty, clarity, and elegance.
Authors of accepted regular papers will be invited (but are not required)
to submit a relevant artifact for evaluation by the artifact evaluation
committee. Authors are encouraged to consult SIGPLAN’s Empirical Evaluation
Guidelines when reporting on empirical results.
*TOOL PAPERS*
Tool papers should not exceed 10 pages, not counting references.
Tool papers should describe system and implementation aspects of a tool
with a large (potential) user base (experiments not required, rehash of
theory strongly discouraged). 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.
Tool papers will follow a single blind review process. They do NOT need to
be anonymized.
Tool papers will be provisionally accepted based on the manuscript. Authors
of provisionally accepted tool papers must submit an artifact for
evaluation by the artifact evaluation committee: final acceptance is
conditional 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.
*INDUSTRIAL EXPERIENCE REPORTS AND CASE STUDIES*
Industrial Experience Reports and Case Studies should not exceed 10 pages,
not counting references.
These papers are expected to describe the use of formal methods techniques
in industrial settings or in new application domains. Papers in this
category do not necessarily need to present original research results but
are expected to contain novel applications of formal methods techniques as
well as an evaluation of these techniques in the chosen application domain.
Such papers are encouraged to discuss the unique challenges of transferring
research ideas to a real-world setting and reflect on any lessons learned
from this technology transfer experience.
Industrial Experience Reports and Case Studies will follow a single blind
review process. They do NOT need to be anonymized.
Authors of accepted Industrial Experience Reports and Case Studies will be
invited (but are not required) to submit a relevant artifact for evaluation
by the artifact evaluation committee.
*CONTACT*
For any questions please contact the PC chairs:
- Arie Gurfinkel <https://ece.uwaterloo.ca/~agurfink> at
arie.gurfinkel(a)uwaterloo.ca
- Vijay Ganesh <https://vganesh1.github.io/> at vganesh(a)gatech.edu
