von Perez Dominguez, Ivan (LARC-D320)[NATIONAL INSTITUTE OF AEROSPACE] via fm-announcements
****************************************************************
CALL FOR (VIRTUAL) PARTICIPATION
The 26th International Conference on
Formal Methods for Industrial Critical Systems
(FMICS 2021)
August 24-26
https://qonfest2021.lacl.fr/fmics21.php<https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fqonfest20…>
Joint event with CONCUR, FORMATS and QEST.
** Free Registration **
****************************************************************
FMICS is the ERCIM Working Group conference on Formal Methods for Industrial Critical Systems, and it is the key conference in the intersection of industrial applications and Formal Methods. The aim of the FMICS conference series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications.
Keynote
-------------------------
- Speaker: Joe Kiniry (Galois Inc. and Free & Fair, US)
- Title: Haunting Tales of Applied Formal Methods from Academia and Industry.
- Abstract: You learn a lot after being a formal methods researcher and practitioner for 25 years. Half of that time was spent in academia, creating formal processes, methodologies, and tools that I hoped I could secretly impact engineers. Half of that time has been spent in industry, working at companies to transition concepts, tools, and technologies in rigorous digital engineering (RDE) with applied formal methods. These days I work at two companies, Galois and Free & Fair, leading R&D in RDE that focus on problems in national security and nationally critical infrastructure. I also work with many of our other Galois spin-outs, such as Muse (now Sonotype Lift) and Niobium Microsystems on these same topics. In this talk I’ll tell a small number of stories about these many years in the field, each of which has, I hope, an actionable nugget of wisdom for the audience at FMICS.
Accepted papers
-------------------------
Davide Basile, Alessandro Fantechi and Irene Rosadi
Formal Analysis of the UNISIG Safety Application Intermediate Sub-Layer
Maurice H. ter Beek, Vincenzo Ciancia, Diego Latella, Mieke Massink and Giorgio Oronzo Spagnolo
Spatial Model Checking for Smart Stations: Research Challenges
Jens Bendisposto, David Geleßus, Michael Leuschel and Fabian Vu
ProB2-UI: A Java-based User Interface for ProB
Roberto Bruttomesso
Intrepid: a Scriptable and Cloud-ready SMT-based Model Checker
Simon Thrane Hansen, Cláudio Gomes, Maurizio Palmieri, Casper Thule, Jaco van de Pol and - Jim Woodcock
Verification of Co-Simulation Algorithms Subject to Algebraic Loops and Adaptive Steps
Hamid Jahanian
Parametric Faults in Safety Critical Programs
Andrej Kiviriga, Ulrik Nyman and Kim Guldstrand Larsen
Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems
Daniel Larraz, Mickaël Laurent and Cesare Tinelli
Merit and Blame Assignment with Kind 2
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré and Hiroaki Inoue
Automated Verification of Temporal Properties of Ladder Programs
Ismail Mendil, Yamine Ait Ameur, Neeraj Kumar Singh, Dominique Méry and Philippe Palanque
Standard Conformance-by-Construction with Event-B
Baptiste Pollien, Xavier Thirioux, Christophe Garion, Gautier Hattenberger and Pierre Roux
Verifying the Mathematical Library of an UAV Autopilot with Frama-C
Riley Roberts, Benjamin Lewis, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty and Zhen Zhang
Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System
Robert Rubbens, Sophie Lathouwers and Marieke Huisman
Modular Transformation of Java Exceptions Modulo Errors
Joshua Schmidt and Michael Leuschel
Improving SMT Solver Integrations for the Validation of B and Event-B Models
Quinn Thibeault, Jacob Anderson, Aniruddh Chandratre, Giulia Pedrielli and Georgios Fainekos
PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems
Bernd Westphal
On education and training in formal methods for industrial critical systems
Registration
-------------------------
There is no registration fee charged to participants. All interested individuals are welcome to attend; however, all attendees must register here:
https://qonfest2021.lacl.fr/registration.php<https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fqonfest20…>
PC Chairs
-------------------------
Alberto Lluch Lafuente (Technical University of Denmark, DK)
Anastasia Mavridou (KBR / NASA Ames Research Center, US)
PC Members
-------------------------
Erika Abraham (RWTH Aachen University, DE)
Massimo Bartoletti (University of Cagliari, IT)
Maurice ter Beek (ISTI-CNR, IT)
Simon Bliudze (INRIA, FR)
Yu-Fang Chen (Academia Sinica, TW)
Silvia Crafa (University of Padova, IT)
Hubert Garavel (INRIA, FR)
Diego Garbervetsky (University of Buenos Aires/CONICET, AR)
Ákos Hajdu (Budapest University of Technology and Economics, HU)
Klaus Havelund (NASA JPL, US)
Anne Haxthausen (Technical University of Denmark, DK)
Fritz Henglein (University of Copenhagen/ Deon Digital , DK)
Fuyuki Ishikawa (National Institute of Informatics, JP)
Xiaoqing Jin (Apple Inc., US)
Joe Kiniry (Galois Inc. and Free & Fair, US)
Thierry Lecomte (ClearSy, FR)
Tiziana Margaria (CSIS, Univ. of Limerick, and LERO, IE)
Diego Marmsoler (University of Exeter, UK)
Radu Mateescu (INRIA, FR)
Dejan Nickovic (Austrian Institute of Technology, AT)
Corina Pasareanu (CMU/ NASA Ames Research Center, US)
Anna Philippou (University of Cyprus, CY)
Jaco van de Pol (Aarhus University, DK)
Clara Schneidewind (Vienna University of Technology, AT)
Cristina Seceleanu (Mälardalen University, SE)
Carolyn Talcott (SRI International, US)
Virginie Wiels (ONERA / DTIM, FR)
Steering Committee
-------------------------
Maurice ter Beek (ISTI-CNR, IT)
Alessandro Fantechi (University of Florence, IT)
Hubert Garavel (INRIA, FR)
Tiziana Margaria (CSIS, Univ. of Limerick, and LERO, IE)
Radu Mateescu (INRIA, FR)
Jaco van de Pol (Aarhus University, DK)
---
To opt-out from this mailing list, send an email to
fm-announcements-request(a)lists.nasa.gov
with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting
fm-announcements-owner(a)lists.nasa.gov
Join the Logica Universalis Webinar!
The next session will be held on Wednesday, August 18 at 4pm CEST with the talk
Logical constants in abstract frameworks<https://link.springer.com/article/10.1007/s11787-018-0206-7> and A Note on Logicality of Generalized Quantifiers<https://link.springer.com/article/10.1007/s11787-021-00271-8>
Tin Perkov<https://urldefense.proofpoint.com/v2/url?u=https-3A__sites.google.com_site_…> (University of Zagreb, Croatia)
Chair: Srećko Kovač<https://urldefense.proofpoint.com/v2/url?u=https-3A__www.ifzg.hr_-7Eskovac_…>, Editorial Board LU
Associate Organization: Croatian Logic Association<https://urldefense.proofpoint.com/v2/url?u=https-3A__www.hlu-2Dcla.com_&d=D…>
presented by its president Srećko Kovač<https://urldefense.proofpoint.com/v2/url?u=https-3A__www.ifzg.hr_-7Eskovac_…>
The Logica Universalis Webinar is a World Seminar Series connected to the journal Logica Universalis<https://www.springer.com/journal/11787/>, the book series Studies in Universal Logic<https://www.springer.com/series/7391> and the Universal Logic Project<https://logica-universalis.org/>. It is an open platform for all scholars interested in the many aspects of logic. (See the full program here<https://www.springer.com/journal/11787/updates/18988758>.)
The sessions take place on Wednesdays at 4pm CEST (click here<https://www.timeanddate.com/worldclock/fixedtime.html?msg=Logica+Universali…> to convert to your timezone). They are held via Zoom and are free to attend. Please register in advance.
Registration is now open!<https://springer.zoom.us/meeting/register/tJMvdu6vrzMiHda_iDhjxw9vA9d7we9gT…>
Each session of the webinar is chaired by a member of the editorial board of the journal Logica Universalis (LU), the book series Studies in Universal Logic (SUL) or an organizer of an event of the Universal Logic Project (ULP). Sessions will start with a short presentation of a logical organization related to the region of the speaker or the topic of the talk. The talk (30 min) will focus on a recently published paper in LU, on a book in SUL, on an event or on the ULP. Talks are followed by a discussion (15 min).
Video recordings of the seminars are uploaded on the YouTube channel Universal Logic Project<https://www.youtube.com/channel/UCPS1c5ApuwjuCV9UjXHUN4w>.
---
To unsubscribe from these notifications for the Logica Universalis Webinar please send a message with 'Unsubscribe' to this e-mail address (antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>).
--
Antje Herbst
Associate Editor Mathematics
Journals
Springer Nature
Tiergartenstraße 17, 69121 Heidelberg, Germany
T +49 62214878984
antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>
www.springernature.com<http://www.springernature.com/>
--
Springer Nature is a leading research, educational and professional publisher, providing quality content to our communities through a range of innovative platforms, products and services. Every day, around the globe, our imprints, books, journals and resources reach millions of people - helping researchers, students, teachers & professionals to discover, learn and achieve.
--
Branch of Springer-Verlag GmbH, Heidelberger Platz 3, 14197 Berlin, Germany
Registered Office: Berlin / Amtsgericht Berlin-Charlottenburg, HRB 91881 B
Directors: Martin Mos, Dr. Ulrich Vest, Dr. Niels Peter Thomas
Today Wednesday August 11 at 16h
(Paris-Madrid-Geneva-Rome-Berlin-Stockholm-Warsaw)
at the Logica Universalis Webinar (LUW) a talk by Yale Weiss based on his
paper recently published in Logica Universalis
A Reinterpretation of the Semilattice Semantics with Applications
https://link.springer.com/article/10.1007/s11787-021-00273-6
Before the talk, as usual in the LUW, there will be a presentation of a
logical organization related to the talk and/or the speaker.
Today it will be the Saul Kripke Center presented by its director, Romina
Padro
https://saulkripkecenter.org/index.php/staff/
The session will be chaired by Melving Fitting, member of the editorial
board of Logica Universalis
http://melvinfitting.org/
To registrate/attend see here:
https://www.springer.com/journal/11787/updates/18988758
Best Wishes
>---------------------------------------------------------------
Prof. Dr. Dr. Jean-Yves Beziau
Organizer of LUW and President of LUA
http://www.logica-universalis.org/LUAD
Join the Logica Universalis Webinar!
The next session will be held on Wednesday, August 11 at 4pm CEST with the talk
A Reinterpretation of the Semilattice Semantics with Applications<https://link.springer.com/article/10.1007/s11787-021-00273-6>
Yale Weiss<https://urldefense.proofpoint.com/v2/url?u=https-3A__yaleweiss.commons.gc.c…> (City University of New York, USA)
Chair: Melvin Fitting<https://urldefense.proofpoint.com/v2/url?u=https-3A__en.wikipedia.org_wiki_…>, Editorial Board LU
Associate Organization: Saul Kripke Center<https://urldefense.proofpoint.com/v2/url?u=https-3A__saulkripkecenter.org_&…>
The Logica Universalis Webinar is a World Seminar Series connected to the journal Logica Universalis<https://www.springer.com/journal/11787/>, the book series Studies in Universal Logic<https://www.springer.com/series/7391> and the Universal Logic Project<https://logica-universalis.org/>. It is an open platform for all scholars interested in the many aspects of logic. (See the full program here<https://www.springer.com/journal/11787/updates/18988758>.)
The sessions take place on Wednesdays at 4pm CEST (click here<https://www.timeanddate.com/worldclock/fixedtime.html?msg=Logica+Universali…> to convert to your timezone). They are held via Zoom and are free to attend. Please register in advance.
Registration is now open!<https://springer.zoom.us/meeting/register/tJMvdu6vrzMiHda_iDhjxw9vA9d7we9gT…>
Each session of the webinar is chaired by a member of the editorial board of the journal Logica Universalis (LU), the book series Studies in Universal Logic (SUL) or an organizer of an event of the Universal Logic Project (ULP). Sessions will start with a short presentation of a logical organization related to the region of the speaker or the topic of the talk. The talk (30 min) will focus on a recently published paper in LU, on a book in SUL, on an event or on the ULP. Talks are followed by a discussion (15 min).
Video recordings of the seminars are uploaded on the YouTube channel Universal Logic Project<https://www.youtube.com/channel/UCPS1c5ApuwjuCV9UjXHUN4w>.
---
To unsubscribe from these notifications for the Logica Universalis Webinar please send a message with 'Unsubscribe' to this e-mail address (antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>).
--
Antje Herbst
Associate Editor Mathematics
Journals
Springer Nature
Tiergartenstraße 17, 69121 Heidelberg, Germany
T +49 62214878984
antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>
www.springernature.com<http://www.springernature.com/>
--
Springer Nature is a leading research, educational and professional publisher, providing quality content to our communities through a range of innovative platforms, products and services. Every day, around the globe, our imprints, books, journals and resources reach millions of people - helping researchers, students, teachers & professionals to discover, learn and achieve.
--
Branch of Springer-Verlag GmbH, Heidelberger Platz 3, 14197 Berlin, Germany
Registered Office: Berlin / Amtsgericht Berlin-Charlottenburg, HRB 91881 B
Directors: Martin Mos, Dr. Ulrich Vest, Dr. Niels Peter Thomas
CALL FOR SHORT CONTRIBUTIONS / POSTERS
19th International Conference on
Relational and Algebraic Methods in Computer Science
RAMiCS 2021
2 to 5 November 2021, Marseille, France
https://ramics19.lis-lab.fr/
Additionally to the standard CfP, RAMiCS is also calling for short
contributions and posters. We are hence calling for presentations of
original, unfinished, already published, or otherwise interesting work
within the topics of the RAMiCS conferences. The submission can be in
the form of a poster, an abstract, a paper submitted to or published
at another conference, etc. Short contributions will *not* be
published in the conference proceedings.
IMPORTANT DATES:
Submission: 29 August 2021
Notification: 5 September 2021
RAMiCS registration: 12 September 2021
INVITED SPEAKERS:
Marcelo Frias, Instituto Tecnológico de Buenos Aires, Argentina
Barbara König, Universität Duisburg-Essen, Germany
Dmitriy Zhuk, Moscow State University, Russia
GENERAL INFORMATION:
Since 1994, the RAMICS conference series has been the main venue for
research on relation algebras, Kleene algebras and similar algebraic
formalisms, and their applications as conceptual and methodological
tools in computer science and beyond.
TOPICS:
We invite short submissions in the general fields of algebras relevant
to computer science and applications of such algebras. Topics include
but are not limited to:
* Theory
- algebras such as semigroups, residuated lattices, semirings,
Kleene algebras, relation algebras and quantales
- their connections with program logics and other logics
- their use in the theories of automata, concurrency, formal languages,
games, networks and programming languages
- the development of algebraic, algorithmic, category-theoretic,
coalgebraic and proof-theoretic methods for these theories
- their formalisation with theorem provers
* Applications
- tools and techniques for program correctness, specification and
verification
- quantitative and qualitative models and semantics of computing
systems and processes
- algorithm design, automated reasoning, network protocol analysis,
social choice, optimisation and control
- industrial applications
SUBMISSION INSTRUCTIONS:
Please send your short submission as a single pdf file to
ramics2021(a)easychair.org
by 29 August 2021.
ORGANIZERS:
Luigi Santocanale, Aix-Marseille University, France
Uli Fahrenberg, École polytechnique, France
Mai Gehrke, Université Côte d’Azur, France
Michael Winter, Brock University, Canada
- Application deadline: Midnight, 31 Aug 2021
- Interview Date: To be confirmed
- Starting date: 1 Oct 2021, or as soon as possible thereafter
- Salary: £35,931-£37,979
- Duration: until February 2023
Applications are invited for the post of Post-Doctoral Research Assistant in the Computer Science Department at Royal Holloway, University of London.
Successful applicants will be working on the EPSRC-funded "Verification of Hardware Concurrency via Model Learning" (CLeVer) project (EP/S028641/1), led by Alexandra Silva (UCL) and Matteo Sammartino (Royal Holloway, University of London).
This is a joint research endeavour involving Royal Holloway University of London, University College London, and ARM, world-leading designer of multi-core chips.
For an informal discussion about the post, please contact Dr. Matteo Sammartino on Matteo.Sammartino(a)rhul.ac.uk.
# Project Description
Digital devices increasingly rely on multi-threaded computation, with sophisticated concurrent behaviour becoming prevalent at any scale. As the complexity of these systems increases, there is a pressing need to automate the assessment of their correctness, especially with respect to concurrency-related aspects. Formal verification provides highly effective techniques to assess the correctness of systems. However, formal models are usually built by humans, and as such can be error-prone and inaccurate.
The CLeVer project aims to:
- develop a novel verification framework that relies on learning techniques to automatically build and verify models of concurrency, with a particular focus on multi-core systems.
- apply the framework to real-world verification tasks, in collaboration with ARM.
# The ideal candidate
We are looking for candidates with a PhD in one of the following areas: model-based testing and verification, formal methods for concurrency, automated analysis of hardware systems. Experience in multiple areas will be valued. Candidates ideally should also have strong programming skills.
# Where to apply
https://jobs.royalholloway.ac.uk/vacancy.aspx?ref=0721-259
Join the Logica Universalis Webinar!
The next session will be held on Wednesday, July 21 at 4pm CEST with the talk
A Venn Diagram System for Universe Without Boundary<https://link.springer.com/article/10.1007/s11787-019-00227-z>
Reetu Bhattacharjee<https://urldefense.proofpoint.com/v2/url?u=https-3A__www.researchgate.net_s…> (Jadavpur University, Kolkata, West Bengal, India)
Chair: Raja Natarajan<https://urldefense.proofpoint.com/v2/url?u=http-3A__www.tcs.tifr.res.in_-7E…>, Editorial Board LU
Associate Organization: Calcutta Logic Circle<https://urldefense.proofpoint.com/v2/url?u=https-3A__sites.google.com_view_…>
Presented by its president Mihir Chakraborty<https://urldefense.proofpoint.com/v2/url?u=https-3A__sites.google.com_site_…>
The Logica Universalis Webinar is a World Seminar Series connected to the journal Logica Universalis<https://www.springer.com/journal/11787/>, the book series Studies in Universal Logic<https://www.springer.com/series/7391> and the Universal Logic Project<https://logica-universalis.org/>. It is an open platform for all scholars interested in the many aspects of logic. (See the full program here<https://www.springer.com/journal/11787/updates/18988758>.)
The sessions take place on Wednesdays at 4pm CEST (click here<https://www.timeanddate.com/worldclock/fixedtime.html?msg=Logica+Universali…> to convert to your timezone). They are held via Zoom and are free to attend. Please register in advance.
Registration is now open!<https://springer.zoom.us/meeting/register/tJMvdu6vrzMiHda_iDhjxw9vA9d7we9gT…>
Each session of the webinar is chaired by a member of the editorial board of the journal Logica Universalis (LU), the book series Studies in Universal Logic (SUL) or an organizer of an event of the Universal Logic Project (ULP). Sessions will start with a short presentation of a logical organization related to the region of the speaker or the topic of the talk. The talk (30 min) will focus on a recently published paper in LU, on a book in SUL, on an event or on the ULP. Talks are followed by a discussion (15 min).
Video recordings of the seminars are uploaded on the YouTube channel Universal Logic Project<https://www.youtube.com/channel/UCPS1c5ApuwjuCV9UjXHUN4w>.
---
To unsubscribe from these notifications for the Logica Universalis Webinar please send a message with 'Unsubscribe' to this e-mail address (antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>).
--
Antje Herbst
Associate Editor Mathematics
Journals
Springer Nature
Tiergartenstraße 17, 69121 Heidelberg, Germany
T +49 62214878984
antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>
www.springernature.com<http://www.springernature.com/>
--
Springer Nature is a leading research, educational and professional publisher, providing quality content to our communities through a range of innovative platforms, products and services. Every day, around the globe, our imprints, books, journals and resources reach millions of people - helping researchers, students, teachers & professionals to discover, learn and achieve.
--
Branch of Springer-Verlag GmbH, Heidelberger Platz 3, 14197 Berlin, Germany
Registered Office: Berlin / Amtsgericht Berlin-Charlottenburg, HRB 91881 B
Directors: Martin Mos, Dr. Ulrich Vest, Dr. Niels Peter Thomas