*****************************************************************************************
24th International Conference on Formal Engineering Methods (ICFEM 2023)
https://formal-analysis.com/icfem/2023/
*****************************************************************************************
## Overview
ICFEM (International Conference on Formal Engineering Methods) is an international leading conference series in formal methods and software engineering. Since 1997, ICFEM has been serving as an international forum for researchers and practitioners who have been seriously applying formal methods to practical applications. Researchers and practitioners, from industry, academia, and government, are encouraged to attend, present their research, and help advance the state of the art. ICFEM is interested in work that has been incorporated into real production systems, and in theoretical work that promises to bring practical and tangible benefit. ICFEM has been hosted in many countries around the world. This year, ICFEM 2023 will be held in Brisbane, Australia (physical) on November 21-24, 2023.
##Topics of Interest
Authors are invited to submit high quality technical papers describing original and unpublished work in all theoretical aspects of software engineering. Topics of interest include, but are not limited to:
- Abstraction, refinement and evolution
- Formal specification and modelling
- Formal verification and analysis
- Model checking and equivalence checking
- Automated and interactive theorem proving
- Formal approaches to software testing and inspection
- Formal methods for self-adaptive systems
- Formal methods for object-oriented systems
- Formal methods for component-based systems
- Formal methods for concurrent and real-time systems
- Formal methods for cloud computing
- Formal methods for cyber-physical systems
- Formal methods for hardware and embedded systems
- Formal methods for software safety and security
- Formal methods for software reliability and dependability
- Development, integration and experiments involving verified systems
- Formal certification of products under international standards
- Formal model-based development and code generation
##Important Dates
- Abstract Submission: May 14, 2023 (AOE)
- Paper Submission: May 21, 2023 (AOE)
- Author Notification: July 30, 2023
- Camera-ready versions: Aug 13, 2023
- Conference: Nov 21-24, 2023
More information can be found on the website of ICFEM 2023: https://formal-analysis.com/icfem/2023/
Submission Instructions
Submission should be done through the ICFEM 2023 submission page, handled by the EasyChair conference system:
https://easychair.org/conferences/?conf=icfem2023
As in previous years, the proceedings will be published in the Springer Lecture Notes in Computer Science series.
Papers should be written in English and should not exceed 16 pages (including references) in the Springer's LNCS format. 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. 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-procee…).
## Organizing Committee
General Co-Chairs
- Jin Song Dong, NUS and Griffith University, Singapore/Australia
- Guangdong Bai, The University of Queensland, Australia
Program Co-Chairs
- Yi Li, Nanyang Technological University, Singapore
- Sofiene Tahar, Concordia University, Canada
Finance Chair
- Zhe Hou, Griffith University, Australia
Publicity Chair
- Cheng-Hao Cai, Monash University at Suzhou, China
- Neeraj Kumar Singh, IRIT-ENSEEIHT, Toulouse, France
Workshop Chair
- Xiaofei Xie, Singapore Management University, Singapore
--
Neeraj Kumar Singh
Associate Professor
INPT-ENSEEIHT/IRIT
F-313, 2 Rue Charles Camichel, BP 7122
31071 Toulouse, CEDEX 7, France
Office: +33 5 34 32 21 82
Email: nsingh(a)enseeiht.fr <mailto:nsingh@enseeiht.fr>
Web Page: http://singh.perso.enseeiht.fr <http://singh.perso.enseeiht.fr/>
************************************************************
Call for Papers
** ATVA 2023 **
24-27 October 2023
Singapore
https://atva-conference.org/2023/
************************************************************
21st International Symposium on Automated Technology for Verification
and Analysis
## Important Dates
* Abstract submission deadline: April 27, 2023 (AoE)
* Paper submission deadline: May 4, 2023 (AoE)
* Paper notification: June 30, 2023 (AoE)
* Camera-ready deadline: July 25, 2023 (AoE)
* Conference: October 24 – October 27, 2023 (UTC +8)
ATVA 2023 is the 21st 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 system
* 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
* Analysis and verification of deep learning systems
* Analysis and verification of blockchain based systems
* Verification in industrial practice
* Synthesis for hardware and software systems
* Applications and case studies
* Automated tool support
## Submissions
ATVA welcomes submissions in the following two categories:
* Regular research papers (16 pages, excluding references)
* Tool papers (6 pages, excluding references)
Submissions must be in Springer's LNCS format. 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. Formatting style files and
further guidelines for formatting can be found at the Springer website.
Adding line numbers (package lineno) is highly recommended.
Tool papers must include information about a URL from where the tool can
be downloaded or accessed on-line for evaluation. The URL must also
contain a set of examples, and a user manual that describes usage of the
tool through examples. In case the tool needs to be downloaded and
installed, the URL must contain instructions for installation of the
tool on Linux/Windows/MacOS.
For (regular and tool) papers reporting experiments, uploading an
artifact on a long-term available platform is recommended (though not
compulsory)
Papers must be submitted through EasyChair.
https://easychair.org/conferences/?conf=atva2023
Accepted papers in both categories will be published in Springer's
Lecture Notes in Computer Science series. At least one author of each
accepted paper is expected to register and present the paper at the
conference.
## Committees
General Chair
* Jin Song DONG, National University of Singapore
Program Co-Chairs
* Jun Sun, Singapore Management University
* Étienne André, Université Sorbonne Paris Nord
Publicity Chair:
* Lei Bu, Nanjing University
Local Organization Chair
* Xiaofei Xie, Singapore Management University
Program committee
* Mohamed Faouzi Atig (Uppsala University)
* Saddek Bensalem (VERIMAG)
* Udi Boker (Reichman University, Herzliya, Israel)
* Lei Bu (Nanjing University)
* Krishnendu Chatterjee (Institute of Science and Technology (IST))
* Yu-Fang Chen (Academia Sinica)
* Chih-Hong Cheng (Fraunhofer IKS)
* Yunja Choi (Kyungpook National University)
* Thao Dang (CNRS/VERIMAG)
* Susanna Donatelli (Dipartimento di Informatica)
* Alexandre Duret-Lutz (EPITA's Research Lab (LRE))
* Bernd Finkbeiner (CISPA Helmholtz Center for Information Security)
* Stefan Gruner (University of Pretoria)
* Osman Hasan (National University of Sciences and Technology (NUST))
* Ichiro Hasuo (National Institute of Informatics)
* Jie-Hong Roland Jiang (National Taiwan University)
* Ondrej Lengal (Brno University of Technology)
* Shang-Wei Lin (Nanyang Technological University)
* Doron Peled (Bar Ilan University)
* Jakob Piribauer (TU Dresden)
* Pavithra Prabhakar (Kansas State University)
* Sasinee Pruekprasert (National Institute of Advanced Industrial
Science and Technology)
* Kristin Yvonne Rozier (Iowa State University)
* Indranil Saha (Indian Institute of Technology Kanpur)
* Ocan Sankur (Univ Rennes)
* Fu Song (School of Information Science and Technology)
* Marielle Stoelinga (University of Twente)
* Michael Tautschnig (Queen Mary University of London)
* Tachio Terauchi (Waseda University)
* Jingyi Wang (Zhejiang University)
* Chao Wang (University of Southern California)
* Bow-Yaw Wang (Academia Sinica)
* Zhilin Wu (Laboratory of Computer Science)
* Lijun Zhang (Institute of Software)
ATVA 2023 is referred by https://conferences-computer.science/
Message from Krishna Nandivada V <nvk(a)iitm.ac.in>, Publicity co-chair ASPLOS 2024.
======================================================================
Synopsis
ASPLOS, the ACM International Conference on Architectural Support for
Programming Languages and Operating Systems, is the premier academic forum
for multidisciplinary computer systems research spanning hardware,
software, and their interaction. It focuses on computer architecture,
programming languages, operating systems, and associated areas such as
networking and storage. ASPLOS 2024 will take place in April 2024 in
California. It has three submission deadlines – spring, summer and fall –
which are meant to encourage authors to submit their papers when they are
ready rather than before. Also, as an alternative to rejection, ASPLOS 2024
will allow the authors of some submissions to choose to apply a major
revision to their submission in order to fix a well-defined list of
problems.
Important Dates and Submission Sites
review cycle spring summer fall
abstract submission 2023-04-13 2023-08-03 2023-11-23
full submission 2023-04-20 2023-08-10 2023-11-30
author response period start 2023-07-11 2023-10-24 2024-02-13
author response period end 2023-07-13 2023-10-26 2024-02-15
notification 2023-08-02 2023-11-15 2024-03-06
camera-ready 2023-09-19 2024-01-09 2024-03-27
submission site link
All deadlines are at 3pm Eastern Time.
Scope and Expectations
The scope of ASPLOS 2024 covers all practical aspects related to the three
main ASPLOS disciplines: computer architecture, programming languages, and
operating systems, as well as closely-related associated areas. We seek
original, high-quality research submissions that improve and further the
knowledge of computer systems, with emphasis on the intersection between
the main ASPLOS disciplines. Research submission may be applicable to
computer systems of any scale, ranging from small, ultra-low power wearable
devices to exascale parallel and cloud computers. We embrace research that
directly targets new problems in innovative ways. The research may target
diverse goals, such as performance, energy, and security. Non-traditional
topics are encouraged, and the review process will be sensitive to the
challenges of multidisciplinary work in emerging areas. We welcome
experience submissions that have a novel aspect and that clearly articulate
the lessons learned. We likewise welcome submissions that convincingly
refute prior published results and common wisdom. We value submissions more
highly if they are accompanied by clearly defined artifacts not previously
available, including traces, original data, source code, or tools developed
as part of the submitted work. We particularly encourage new ideas and
approaches.
Alphabetically sorted areas of interest related to practical aspects of
computer architecture, programming languages, and operating systems include
but are not limited to:
□ Existing, emerging, and nontraditional compute platforms at all scales
□ Heterogeneous architectures and accelerators
□ Internet services, cloud computing, and datacenters
□ Memory, storage, networking, and I/O
□ Power, energy, and thermal management
□ Profiling, debugging, and testing
□ Security, reliability, and availability
□ Systems for enabling parallelism and computation on big data
□ Virtualization and virtualized systems
A good submission will typically: motivate a significant problem; propose a
practical solution or approach that makes sense; demonstrate not just the
pros but also the cons of the proposal using sound experimental methods;
explicitly disclose what has and has not been implemented; articulate the
new contributions beyond previous work; and refrain from overclaiming,
focusing the abstract and introduction sections primarily on the difference
between the new proposal and what is already available. Submissions will be
judged on relevance, novelty, technical merit, and clarity. Submissions are
expected to avoid committing “benchmarking crimes,” and they must follow
all the policies specified below.
Resubmissions
Authors of resubmitted work should describe in a separate note – uploaded
to the submission site – the changes since the previous submission(s). This
description helps reviewers who may have reviewed a previous draft of the
work to appreciate any improvements to the currently submitted work. Please
try to limit this document to one page.
Submissions rejected from ASPLOS must not be submitted to the next two
subsequent review cycles. The following table details when ASPLOS ’23 and
ASPLOS ’24 rejections can be resubmitted to ASPLOS ’24 and ASPLOS ’25.
if rejected from must not resubmit to may resubmit to
2023 spring – 2024 spring or later
2023 summer 2024 spring 2024 summer or later
2023 fall 2024 spring & summer 2024 fall or later
2024 spring 2024 summer & fall 2025 spring or later
2024 summer 2024 fall & 2025 spring 2025 summer or later
2024 fall 2025 spring & summer 2025 fall or later
The above rules are strict and hold even if your submission has undergone
extensive revisions. (We apologize to authors of any ASPLOS ‘23 rejections
who might not have expected to be affected by this policy.)
Major Revision Option
When the outcome of a review cycle is publicized, some submissions will be
associated with a “revise and resubmit” decision. The authors of such
submissions will be given the opportunity to apply a major revision to
their work and resubmit it after around 6 weeks. These submissions will be
provided with clear and actionable reviewer feedback for their revision,
and they will be typically reviewed by the same reviewers as the original
submission. If the revision requirements are satisfactorily met, the
revised submission will be accepted.
Artifact Evaluation
Artifact evaluation will continue in 2024 as has become a tradition at
ASPLOS. More details will become available later.
======================================================================
Call For Papers (Deadline Extension)
THE 11th INTERNATIONAL CONFERENCE ON NETWORKED SYSTEMS (NETYS 2023)
May 22-24, 2023, Marrakech, Morroco
http://www.netys.net
Aim and Scope:
--------------
NETYS aims to bring together researchers and engineers from both the theory and practice of distributed and networked systems. The scope of the conference covers all aspects related to the design and the development of these systems, including, but not restricted to, concurrent and distributed algorithms, parallel/concurrent/distributed programming, multi-core architectures, distributed databases, cloud systems, networks, security, formal verification, etc.
NETYS will provide a forum to report on best practices and novel algorithms, results and techniques on networked systems. Original research contributions and experience papers on the principles, design, implementation, modeling, analysis, verification, and application of networked systems are solicited.
Topics of interest include (but are not limited to):
- Cloud systems and data centers
- Parallel/concurrent/distributed algorithms and programming
- Cyber-physical systems
- Distributed databases, embedded and operating systems
- Distributed ledgers and blockchain technologies
- Event-based systems
- Formal verification
- Internet of Things, 5G, URLLC
- Mobile, wireless, ad-hoc and sensor networks
- Game Theory, Mechanisms design
- Overlay and peer-to-peer infrastructures
- Decentralized Artificial Intelligence/Machine Learning
- Multi-core architectures and multithreaded applications
- Security and privacy
- Self-stabilizing, self-organizing, and autonomic systems
- Social networks
- Static and dynamic analysis and testing
- Collaborative intelligent systems
Confirmed Keynote Speakers:
---------------------------
Gilles Barthe (Max Planck Institute for Security and Privacy, Germany)
Nikolaj Bjorner (Microsoft Research, USA)
Nate Foster (Cornell University, USA)
Iordanis Kerenidis (University Paris Diderot, France)
Peter Müller (ETH Zurich, Switzerland)
Ruzica Piskac (Yale University, USA)
Important dates (all deadlines are at 23:59 AoE):
-----------------
- Abstract submission: March 22, 2023 (recommended)
- Paper submission: March 29, 2023
- Notifications: April 27, 2023
- Camera-ready submission: May 11, 2023
- Conference dates: May 22-24, 2023
Publication:
------------
Springer's Lecture Notes in Computer Science series will publish the proceedings of the conference (https://www.springer.com/gp/computer-science/lncs). It is required that each accepted paper be presented at the conference by one of its authors.
Submission Instructions:
------------------------
All submissions must follow the LNCS template and be written in English.
Full papers are allowed a maximum of 15 pages in the LNCS format, excluding bibliographic references, whereas short papers are allowed a maximum of 5 pages (in the same format).
Papers exceeding these limits may be rejected without review. A clearly marked appendix can be included for supplementary materials but the appendix will be read at the discretion of the reviewers; therefore, the main body of the paper should contain sufficient details to assess its contributions.
Submission of papers is via EasyChair: https://easychair.org/conferences/?conf=netys2023
Program Chairs:
David Mohaisen <mohaisen(a)ucf.edu>
Thomas Wies <wies(a)cs.nyu.edu>
Dear all,
The next talk in the IARCS Verification Seminar Series will be given by
Markus Kuppe, a Principal Research Software Development Engineer in the
Research In Software Engineering group at Microsoft Research, Redmond. The
talk is scheduled on Tuesday, March 14, at 1900 hrs IST (add to Google
calendar
<https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MzdlMXZ1c2…>).
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: TLA+: The Tools, The Language, and The Application
Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)
Abstract: TLA+ is a language for formally specifying and verifying discrete
systems, including distributed algorithms. Users describe the system as a
state machine, written in a language based on mathematical set theory and
temporal logic, which also serves to express safety and liveness
properties. TLA+ comes with tools for computer-assisted verification,
including two model checkers and an interactive proof system. TLA+ is used
in academia and industry, e.g., to verify data consistency in cloud
applications.
This talk will cover the theory behind TLA+ and how practitioners can write
TLA+ specifications with the help of verification tools. Additionally, we
will discuss known limitations of the tools and outline current and future
research opportunities.
Bio: Markus Kuppe is a Principal Research Software Development Engineer in
the Research In Software Engineering group at Microsoft Research, Redmond.
His focus is on making specification-driven development (with TLA+) more
popular among engineers. This includes scaling verification to real-world
problems and building tools to combine specification-driven development
with established software engineering processes.
Edge computing, as the convergence of computing and communications executed
close to data collection and places of storage and application, provides a
paradigm that offers several research and application opportunities across
a wide range of domains. At the same time, it raises many fundamental and
unprecedented research and development problems and challenges. The 2023
IEEE International Conference on Edge Computing and Communications (IEEE
EDGE 2023 - https://conferences.computer.org/edge/2023/) aims to continue
to be recognized a prime international forum for both researchers and
industry practitioners to exchange the latest fundamental advances in state
of the art and practice of edge computing, identify emerging research
topics, and define the future of edge computing. IEEE EDGE is affiliated
with IEEE World Congress on Services (SERVICES -
https://conferences.computer.org/services/2023/).
IEEE EDGE 2023 will feature a comprehensive high-quality technical program
including research track, tutorial and demonstration. IEEE EDGE 2023 will
also include an attractive industry program aimed at practitioners, with
keynotes and panels from prominent research, industry leaders, and
technological exhibits. IEEE EDGE 2023 invites original papers addressing
all aspects related to edge computing theories, technologies and
applications. Topics of interest include but are not limited to the
following:
· Edge Computing Architectures
· Edge Computing and Communications Theories
· Edge Computing and Network Functions Virtualization
· Edge Computing in Multi-cloud environments
· Signal Processing in Edge Computing
· Edge Access Networks & Systems
· Services for Edge Computing
· CPU/GPU and Hardware for Edge Computing
· AI Enabled Edge Computing
· Edge Centric Convergence of IoT & Cloud Computing
· Collaborative Edge & Cloud Computing
· Storage and Caching at the Edge
· QoS & QoE at the Edge
· Artificial Intelligence and ML at the Edge
· Edge Computing for Vehicular System & Network
· Edge Computing for 5G/6G Network & Systems
IMPORTANT DATES (ANYWHERE ON EARTH) – UPDATED!
● March 25, 2023: Easy Chair closes for submissions (e.g., HARD
submission deadline)
● April 23, 2023: Acceptance notification
● July 2-8, 2023: SERVICES Congress in Chicago
ORGANISING TEAM
IEEE EDGE 2023 GENERAL CHAIRS
Andrzej Goscinski, Deakin University
Omer Rana, Cardiff University
IEEE EDGE 2023 PROGRAM CHAIRS
Flavia Delicato, Fluminense Federal University
Nirmit Desai, IBM Research, TJ Watson Research Center
IEEE EDGE 2023 PUBLICITY CHAIRS
Nitin Auluck, Indian Institute of Technology, Ropar
Luiz F. Bittencourt, University of Campinas, Brazil
Antonino Galletta, University of Messina, Italy
Gautam Srivastava, Brandon University, Canada
--
Dr. Nitin Auluck / डॉ. नितिन औलक | Associate Professor / सह - प्राध्यापक
Room #114, S. Ramanujan Block / कमरा #११४, एस. रामानुजम ब्लॉक
Department of Computer Science & Engineering / कंप्यूटर विज्ञान और
अभियांत्रिकी विभाग
Indian Institute of Technology Ropar / भारतीय प्रौद्योगिकी संस्थान
रोपड़ | Rupnagar,
Punjab, India, 140001 / रूपनगर, पंजाब, भारत, १४०००१
nitin(a)iitrpr.ac.in | http://www.iitrpr.ac.in/cse/nitin
--
**CONFIDENTIALITY NOTICE: The
contents of this email message and any
attachments are intended solely
for the addressee(s) and may contain
confidential and/or privileged
information and may be legally protected
from disclosure. If you are not
the intended recipient of this message or
their agent, or if this
message has been addressed to you in error, please
immediately alert the
sender by reply email and then delete this message
and any attachments.
If you are not the intended recipient, you are hereby
notified that any
use, dissemination, copying, or storage of this message
or its
attachments is strictly prohibited.*
*
ETAPS 2023 EXTENDED STAY SUPPORT SCHEME
The ETAPS 2023 conference (European joint conferences on theory &
practice of software), organized in Paris from 22nd to 27th April 2023,
offers an Extended Stay Support Scheme (ESSS) aiming at enhancing
scientific collaborations and diminishing the carbon footprint of
scientific research activities, following similar initiatives at
HIGHLIGHTS and ICALP. ETAPS 2023 attendees are encouraged to combine
their visit to Paris with collaborations with local researchers.
In a nutshell: interested individual participants to ETAPS can get a
financial support from interested labs to stay longer "near" Paris,
supported by labs throughout France or neighboring countries (Belgium
and Switzerland).
This support scheme is primarily intended for participants traveling
long distances and must be combined with an attendance to ETAPS 2023.
Upon acceptation, research institutes involved in this mechanism will
cover standard expenses (accommodation and traveling fees, plane
excluded) and will provide material support for research activities.
How to apply to the ETAPS 2023 Extended Stay Support Scheme?
Application to the ETAPS 2023 Extended Stay Support Scheme is made by
two persons, a visitor and a local collaborator and should be sent to
the contact person in the hosting research institute. The application
should include:
- The name of the visitor (the ETAPS attendant) mentioning their
affiliation, city and country of origin
- The name of the local collaborator
- The dates of the visits
- Few lines describing the subject of the collaboration
The ETAPS organizers are NOT involved in this selection process.
Web page: https://etaps.org/2023/esss/
Specific constraints:
- For applying, the visitor should attend ETAPS 2023
- Dates of the visit do not have to be adjacent to the conference dates
as long as the applicant avoids traveling by plane in between
- If too many applications are received, further criteria of selection
may have to be applied by the inviting labs, such as favoring long
distance participants or applying "first come first served" policy.
The research labs participating to the scheme are so far:
* CRIStAL, Lille (https://www.cristal.univ-lille.fr/?rubrique9)
Contact: <Patrick Baillot patrick.baillot(a)univ-lille.fr>
* EPFL, SYSTEMF, Lausanne (https://www.epfl.ch/): Contact: Clément
Pit-Claudel (https://pit-claudel.fr/clement/)
* Irif, Université Paris-Cité, Paris (https://www.irif.fr/).
Contact: Thomas Colcombet <thomas.colcombet(a)irif.fr>
* LAAS, Toulouse (https://www.laas.fr/public/en). Contact: Silvano
Dal Zilio <dalzilio(a)laas.fr>
* LABRI, Bordeaux (https://www.labri.fr/en). Contact: Cyril
Gavoille <gavoille(a)labri.fr>
* LIP, ENS Lyon (http://www.ens-lyon.fr/LIP/) Contact: Denis
Kuperberg <denis.kuperberg(a)ens-lyon.fr>
* Lip6, Sorbonne Université, Paris
(https://www.lip6.fr/recherche/index.php), and co-organizer of ETAPS
2023. Contact: Fabrice Kordon <Fabrice.Kordon(a)lip6.fr>
* LIPN, Université Sorbonne Paris Nord, Villetaneuse
(https://lipn.univ-paris13.fr/), and co-organizer of ETAPS 2023.
Contact: Étienne André <Andre.Etienne(a)lipn13.fr>
* LiS, Marseille (https://www.lis-lab.fr/). Contact: Pierre-Alain
Reynier <pierre-alain.reynier(a)lis-lab.fr>
* LMF, Université Paris-Saclay, Saclay (https://lmf.cnrs.fr/).
Contact: Dietmar Berwanger <dwb(a)lsv.fr>
* LORIA, Université de Lorraine & Inria, Nancy
(https://www.loria.fr/en/). Contact: Stephan Merz <stephan.merz(a)loria.fr>
* LS2N, Université de Nantes (SLS axis:
https://www.ls2n.fr/pole/SLS/). Contact: Dalila Tamzalit
<dalila.tamzalit(a)univ-nantes.fr>
* LSL, CEA List, Saclay (https://pyrat-analyzer.com/). Contact:
CHIHANI Zakaria <Zakaria.CHIHANI(a)cea.fr>
* Telecom Paris
(https://www.telecom-paris.fr/en/research/laboratories/information-processin…).
Contact: Théo Zimmermann <theo.zimmermann(a)telecom-paris.fr>
* ULB, Team "Formal Methods and Verification"
(https://verif.ulb.ac.be/), Brussels, Belgium. Contact: Emmanuel Filiot
<efiliot(a)ulb.be>
* Verimag, Grenoble (https://www-verimag.imag.fr/). Contact:
verimag-direction(a)univ-grenoble-alpes.fr
Other research labs may be added to this list.
For applying as a researcher, please contact the research lab of interest.
For applying as a research unit, please get in touch with
Andre.Etienne(a)lipn13.fr
Dear all,
The next talk in the IARCS Verification Seminar Series will be given by
Markus Kuppe, a Principal Research Software Development Engineer in the
Research In Software Engineering group at Microsoft Research, Redmond. The
talk is scheduled on Tuesday, March 14, at 1900 hrs IST (add to Google
calendar
<https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MzdlMXZ1c2…>).
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: TLA+: The Tools, The Language, and The Application
Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)
Abstract: TLA+ is a language for formally specifying and verifying discrete
systems, including distributed algorithms. Users describe the system as a
state machine, written in a language based on mathematical set theory and
temporal logic, which also serves to express safety and liveness
properties. TLA+ comes with tools for computer-assisted verification,
including two model checkers and an interactive proof system. TLA+ is used
in academia and industry, e.g., to verify data consistency in cloud
applications.
This talk will cover the theory behind TLA+ and how practitioners can write
TLA+ specifications with the help of verification tools. Additionally, we
will discuss known limitations of the tools and outline current and future
research opportunities.
Bio: Markus Kuppe is a Principal Research Software Development Engineer in
the Research In Software Engineering group at Microsoft Research, Redmond.
His focus is on making specification-driven development (with TLA+) more
popular among engineers. This includes scaling verification to real-world
problems and building tools to combine specification-driven development
with established software engineering processes.