Call for Participation
Symposium
Logic and Algorithms in Computational Linguistics 2021 (LACompLing2021)
15 - 17 December 2021, Online
https://staff.math.su.se/rloukanova/LACompLing2021-web/
Online streaming by CNRS, Montpellier, France
https://malin2021.sciencesconf.org
LACompLing2021 is part of the week
Mathematical Linguistics (MALIN) 2021,
Université de Montpellier, LIRMM, CNRS, Montpellier, France
13--17 December 2021, Online
====
PROGRAM
WEDNESDAY DECEMBER 15 / Wed 15 Dec
09:00-9::40 Wed 15 Dec
Stefan Müller (Humboldt-Universität zu Berlin, Germany)
The CoreGram Project: Deriving Crosslinguisitc Generalizations with HPSG
Grammars of Multiple Languages (Invited Talk)
9:40-10:20 Wed 15 Dec
Lars Hellan (Norwegian University of Science and Technology, Norway)
A Unified Valence Resource (Invited Talk)
10:20-10:40 Break
10:40-11:00 Wed 15 Dec
Luuk Suurmeijer (Heinrich Heine University Düsseldorf), Noortje Venhuizen
(Saarland University) and Harm Brouwer (Saarland University, Germany)
Compositionality in Distributional Formal Semantics
11:00-12:00 Wed 15 Dec
Michael Moortgat (Utrecht University, Netherlands)
Dependency Relations, Modalities and the Syntax-Semantics Interface
(Keynote Talk)
12:00-13:30 Lunch break
13:30-14:10 Wed 15 Dec
Stepan Kuznetsov (Steklov Mathematical Institute, RAS, Russia)
Complexity of the Lambek Calculus and Its Extensions (Invited Talk)
14:10-14:30 Wed 15 Dec
Renhao Pei (Utrecht University, Netherlands)
Generating Pragmatically Appropriate Sentences from Propositional Logic:
the Case of Conditional and Biconditional
14:30-15:30 Wed 15 Dec
Christian Retoré (Université de Montpellier and LIRMM-CNRS, France)
Inferentialism and Natural Language Semantics, with a Focus on Quantifiers
(Keynote Talk)
15:30-15:50 Break
15:50-16:30 Wed 15 Dec
Denis Bechet (LS2N - University of Nantes, France) and Annie Foret (IRISA,
University of Rennes 1, France)
Categorial Dependency Grammars: Analysis and Learning (Invited Talk)
16:30-17:30 Wed 15 Dec
Tracy King (Adobe, United States)
White Roses, Red Backgrounds: Bringing Structured Representations to Search
(Keynote Talk)
THURSDAY DECEMBER 16 / Thu 16 Dec
09:00-09:20 Thu 16 Dec
Hitomi Yanaka (The University of Tokyo, Japan)
Towards Compositional Semantics and Inference System for Telicity
09:20-09:40 Thu 16 Dec
Daisuke Bekki, Ribeka Tanaka and Yuta Takahashi
(Ochanomizu University, Japan)
Integrating Deep Neural Network with Dependent Type Semantics
09:40-10:20 Thu 16 Dec
Zhaohui Luo (Dept of Computer Science, Royal Holloway, Univ of London,
United Kingdom)
Universes in Type-Theoretical Semantics (Invited Talk)
10:20-10:40 Break
10:40-11:20 Thu 16 Dec
Kristina Liefke (Ruhr University Bochum, Germany)
Meaning-Driven Combinatorial Restrictions and 'imagine *whether' (Invited
Talk)
11:20-12:00 Thu 16 Dec
Alexey Stukachev (Sobolev Institute of Mathematics, Novosibirsk State
University, Russia)
Generalized Computability and Effective Model Theory in Mathematical
Linguistics (Invited Talk)
12:00-13:30 Lunch break
13:30-14:30 Thu 16 Dec
Richard Moot, (Université de Montpellier and LIRMM-CNRS, Montpellier, France
Graph Rewriting as a Universal Proof Theory for Modern Type-Logical
Grammars (Keynote Talk)
14:30-15:30 Thu 16 Dec
Randy Harris (University of Waterloo, Canada)
Rhetorical Figures as Algorithms (Keynote Address)
FRIDAY DECEMBER 17 / Fri 17 Dec
09:00-10:00 Fri 17 Dec
Aarne Ranta (University of Gothenburg, Sweden)
Abstract Wikipedia and Vastly Multilingual Natural Language Generation
(Keynote Talk)
10:00-10:20 Fri 17 Dec
Inari Listenmaa (Singapore Management University, Singapore),
Martin Strecker (Singapore Management University, Singapore) and
Warrick Macmillan (University of Gothenburg, Sweden)
Natural Language Generation and Processing for the Legal Domain
10:20-10:40 Break
10:40-11:20 Fri 17 Dec
Bjoern Jespersen (Utrecht University, Netherlands)
Impossibilities without Impossibilia (Invited Talk)
11:20-12:00 Fri 17 Dec
Marie Duzi (VSB-Technical University of Ostrava, Czechia)
Questions and Answers on Dynamic Activities of Agents (Invited Talk)
12:00-13:30 Lunch break
13:30-13:50 Fri 17 Dec
Symon Jory Stevensguille (The Ohio State University, United States)
Decomposing Events into GOLOG
13:50-15:30 Fri 17 Dec
Lasha Abzianidze (Utrecht University, Netherlands)
How to Train a Theorem Prover for Natural Language Inference (Invited Talk)
15:30-16:00 Break
16:00-17:00 Fri 17 Dec
Larry Moss (Indiana University Mathematics Department, United States)
Monotonicity in Natural Language Inference: Theory and Practice (Keynote
Talk LACL / LACompLing2021)
====
Join the Logica Universalis Webinar!
The next session will be held on Wednesday, December 8 at 4pm CET with the talk
Decolonizing “Natural Logic”<https://link.springer.com/chapter/10.1007/978-3-030-58446-7_2> (Chapter of Logical Skills<https://www.springer.com/gp/book/9783030584450>)
Scott Pratt<https://urldefense.proofpoint.com/v2/url?u=https-3A__philosophy.uoregon.edu…> (University of Oregon, USA)
Chair: Julie Brumberg-Chaumont<https://urldefense.proofpoint.com/v2/url?u=https-3A__cnrs.academia.edu_juli…> and Claude Rosental<https://urldefense.proofpoint.com/v2/url?u=http-3A__cems.ehess.fr_index.php…>
Editors of the book Logical Skills<https://www.springer.com/gp/book/9783030584450>
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 CET (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
von Titolo, Laura (LARC-D320)[NATIONAL INSTITUTE OF AEROSPACE] via fm-announcements
*** Call for Participation ***
*** Certified Programs and Proofs (CPP) 2022 ***
- Early registration deadline: 3 January 2022
- Getting a visa: https://popl22.sigplan.org/attending/visa-information
- Registration: https://popl22.sigplan.org/attending/registration
- Further reduced student participation fee: see below
- Accommodation: https://popl22.sigplan.org/venue/POPL-2022-venue
Certified Programs and Proofs (CPP) is an international conference on
practical and theoretical topics in all areas that consider formal
verification and certification as an essential paradigm for their
work. CPP spans areas of computer science, mathematics, logic, and
education.
CPP 2022 (https://popl22.sigplan.org/home/CPP-2022) will be held on
17-18 January 2022 and will be co-located with POPL 2022. CPP 2022 is
sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG, and
supported by a diverse set of industrial sponsors.
Similarly to other events collocated with POPL 2022, CPP will take
place as an in-person event at the Westin Philadelphia (99 South 17th
Street at Liberty Place, 19103 Philadelphia), and will require
attendees to provide proof of vaccination (details will be available
soon). Authors who are unable to attend CPP in person will be able to
present remotely. All talks will be recorded, and all recordings will
be available either as a livestream or soon afterwards.
For more information about this edition and the CPP series, please
visit https://popl22.sigplan.org/home/CPP-2022
### Invited talks
* June Andronick (UNSW Sydney). The seL4 verification: the art and
craft of proof and the reality of commercial support
* Andrew W. Appel (Princeton). Coq’s vibrant ecosystem for
verification engineering
* Cesar Munoz (Currently at AWS, Formerly at NASA, USA). Structural
Embeddings Revisited
### Accepted papers
The list of accepted papers is available at
https://popl22.sigplan.org/home/CPP-2022#event-overview
### Subsidized student registration
To facilitate in-person participation of undergraduate and graduate
students who require financial assistance, CPP 2022 offers the
opportunity to register at a special reduced rate, determined on a
case-by-case basis, and implemented using a special-purpose
registration code on POPL's registration website. Students wishing to
apply for such support may do so by sending an email to the CPP conference
co-chairs (Beringer and Krebbers, see below for their email)
preferably by December 24, 2021, with a brief description of their
situation. Notifications will be sent out at most one week later;
hence, students who cannot be supported will still have the
opportunity to register at the publicly available reduced rate, which
is available until January 3rd. Applications arriving after December
24th will be considered only in exceptional cases. Students who
already receive registration support for PLMW or are supported by
SIGPLAN PAC are not eligible.
CPP's student support is made possible by our generous industrial supporters:
https://popl22.sigplan.org/home/CPP-2022
### Contact
For any questions please contact the chairs:
Andrei Popescu <mailto:a.popescu@sheffield.ac.uk> (PC co-chair)
Steve Zdancewic <mailto:stevez@seas.upenn.edu> (PC co-chair)
Lennart Beringer <mailto:eberinge@cs.princeton.edu> (conference co-chair)
Robbert Krebbers <mailto:mail@robbertkrebbers.nl> (conference co-chair)
---
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
The University of Sheffield is seeking candidates with an outstanding record of scholarship in the logical and semantic foundations of computing, and in particular hardware and software verification. You will work within the Verification Group, a well-established research group in the Department of Computer Science which currently hosts six members of staff and one Research Assistant.
Current research ranges from the mathematical and logical foundations of computing to practical verification methods and tools to support these. Particular strengths of the group include the semantic, algebraic and categorical foundations of concurrent and distributed systems, computational logics, finite model theory and descriptive complexity, formal methods for hardware and software systems, verification of quantitative systems, verification of hybrid and cyber physical systems, verification of multi-core programs and weak memory models, as well as interactive and automated theorem proving. To expand and complement these strengths we encourage applications in any of the fields mentioned above, and beyond.
Details: https://www.jobs.ac.uk/job/CLF125/lecturer-in-verification
*******************************************************
* PostDoc position in Computer Science Logic
* University of Sheffield, UK
* Salary: £32,344 to £40,927 per annum (Grade 7)
* Deadline: 3rd January 2022
* Starting date: ASAP / negotiable
* Duration: Until 31.10.2023 (very likely extension to a total of 26 months)
* Details: https://www.jobs.ac.uk/job/CLB973/research-associate-in-computer-science-lo…
*******************************************************
I am looking for a PostDoc to join the Verification group (https://www.sheffield.ac.uk/dcs/research/groups/verification <https://www.sheffield.ac.uk/dcs/research/groups/verification>) of The University of Sheffield (https://www.sheffield.ac.uk/dcs <https://www.sheffield.ac.uk/dcs>) to work with me in my DFG funded project "Logical approach to quantum mechanics and contextuality" (http://www.virtema.fi/dfg).
The project relates to logical foundations of probabilistic data, complexity theory utilising real numbers, and logical approach to quantum information theory utilising the newly discovered connections to probabilistic team semantics. Candidates with expertise in finite model theory, logic in computer science, or foundations of quantum information theory are in particular encouraged to apply.
Interested candidates are encouraged to contact me directly by email for further details (j.t.virtema(a)sheffield.ac.uk). For more details on the topic, the candidate may refer to the subsection “Probabilistic Logics and Metafinite Model Theory” at http://www.virtema.fi/ <http://www.virtema.fi/>.
Full advert below, and in https://www.jobs.ac.uk/job/CLB973/research-associate-in-computer-science-lo… <https://www.jobs.ac.uk/job/CLB973/research-associate-in-computer-science-lo…>.
Best wishes,
Jonni
------------
Are you interested in working for a top computer science department in the UK? Would you like to contribute to work on logical foundations of probabilistic data and complexity theory utilising real numbers? Are you interested in a logical approach to quantum information theory? Do you have expertise in finite model theory, logic in computer science, or foundation of quantum information theory? Applications are invited for a Research Associate to work with Dr Virtema in a German Research Foundation (DFG) funded project “Logical approach to quantum mechanics”.
The position is situated within the theory theme of the Department of Computer Science at The University of Sheffield, which is composed of the verification and algorithms research groups encompassing around 10 academic staff. Within the project, you will have the opportunity to work with leading groups and academics (e.g., from University of Helsinki, Hasselt University, Leibniz Universität Hannover, University of Oxford, and UC Santa Cruz) that have significant expertise in finite model theory, complexity theory, on the logical foundations of databases and quantum information theory, and on theoretical computer science as a whole.
With researchers at the partner universities, you will develop theory related probabilistic team semantics, descriptive complexity of real number computation and/or their connections to quantum information theory. Collaboration with project partners will provide you with the opportunity to further extend and develop your knowledge in a range of areas associated with finite model theory and logical foundations.
Candidates are expected to hold a PhD in a relevant subject (or be close to completion). You should also have experience in finite model theory, logic in computer science, or foundations of quantum information theory. Familiarity in mathematics related to real numbers, quantum information theory or logics with team semantics is seen as an advantage. You will need to have good communication skills in order to disseminate your findings in international conferences and workshops.
For informal inquiries about the job, contact: Dr. Jonni Virtema on j.t.virtema(a)sheffield.ac.uk. More information can also be found on his academic website www.virtema.fi.
We’re one of the best not-for-profit organisations to work for in the UK. The University’s Total Reward Package includes a competitive salary, a generous Pension Scheme and annual leave entitlement, as well as access to a range of learning and development courses to support your personal and professional development.
We build teams of people from different heritages and lifestyles from across the world, whose talent and contributions complement each other to greatest effect. We believe diversity in all its forms delivers greater impact through research, teaching and student experience.
To find out what makes the University of Sheffield a remarkable place to work, watch this short film: www.youtube.com/watch?v=7LblLk18zmo, and follow @sheffielduni and @ShefUniJobs on Twitter for more information.
[Please distribute. Apologies for multiple postings]
CALL FOR PAPERS
WoLLIC 2022
28th Workshop on Logic, Language, Information and Computation
September 20 to 23, 2022
Iași, Romania
ORGANISATION
Faculty of Computer Science, Alexandru Ioan Cuza University, Romania
Centro de Informática, Universidade Federal de Pernambuco, Brazil
CALL FOR PAPERS
WoLLIC is an annual international forum on inter-disciplinary research
involving formal logic, computing and programming theory, and natural
language and reasoning. Each meeting includes invited talks and tutorials
as well as contributed papers. The twenty-eighth WoLLIC will be held at the
Faculty of Computer Science, Alexandru Ioan Cuza University, Iași, Romania,
September 20 to 23, 2022. It is scientifically sponsored by the
Association for Symbolic Logic (ASL), the Interest Group in Pure and
Applied Logics (IGPL), the The Association for Logic, Language and
Information (FoLLI), the European Association for Theoretical Computer
Science (EATCS) (tbc), and the Sociedade Brasileira de Lógica (SBL).
ABOUT THE LOCATION
Iași https://www.uaic.ro/en/iasi-2/
PAPER SUBMISSION
Contributions are invited on all pertinent subjects, with particular
interest in cross-disciplinary topics. Typical but not exclusive areas of
interest are: foundations of computing, programming and Artificial
Intelligence (AI); novel computation models and paradigms; broad notions of
proof and belief; proof mining, type theory, effective learnability and
explainable AI; formal methods in software and hardware development;
logical approach to natural language and reasoning; logics of programs,
actions and resources; foundational aspects of information organization,
search, flow, sharing, and protection; foundations of mathematics;
philosophical logic; philosophy of language.
Proposed contributions should be in English, and consist of a scholarly
exposition accessible to the non-specialist, including motivation,
background, and comparison with related works. Articles should be written
in the LaTeX format of LNCS by Springer (see author's instructions at
http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0). They must
not exceed 12 pages, with up to 5 additional pages for references and
technical appendices. The paper's main results must not be published or
submitted for publication in refereed venues, including journals and other
scientific meetings.
It is expected that each accepted paper be presented at the meeting by one
of its authors. (At least one author is required to pay the registration
fee before granting that the paper will be published in the proceedings.)
Papers must be submitted electronically at the WoLLIC 2022 EasyChair
website https://easychair.org/conferences/?conf=wollic2022.
PROCEEDINGS
The proceedings of WoLLIC 2022, including both invited and contributed
papers, will be published in advance of the meeting as a volume in
Springer's LNCS series. In addition, abstracts will be published in the
Conference Report section of the Logic Journal of the IGPL, and selected
contributions will be published (after a new round of reviewing) as a
special post-conference WoLLIC 2022 issue of a scientific journal (to be
confirmed).
INVITED SPEAKERS
(tba)
IMPORTANT DATES
April 30, 2022: Abstract deadline
May 7, 2022: Full paper deadline
June 15, 2022: Author notification
June 26, 2022: Final version deadline (firm)
PROGRAMME COMMITTEE
Agata Ciabattoni (Technische Universität Wien) (Co-Chair)
Diana Costa (University of Lisbon)
Hans van Ditmarsch (Open University of the Netherlands)
Roman Kuznets (Technische Universität Wien)
João Marcos (Univ Federal do Rio Grande do Norte)
Larry Moss (Indiana University Bloomington)
Valeria de Paiva (Topos Institute and PUC-Rio)
Elaine Pimentel (Univ Federal do Rio Grande do Norte) (Co-Chair)
Revantha Ramanayake (University of Groningen)
Mehrnoosh Sadrzadeh (University College London)
Alexandra Silva (Cornell University)
Alex Simpson (University of Ljubljana)
Sonja Smets (University of Amsterdam)
Alwen Tiu (The Australian National University)
Leon van der Torre (University of Luxembourg)
Andrea Aler Tubella (Umeå University)
Andres Villaveces (Universidad Nacional de Colombia)
Renata Wassermann (Universidade de São Paulo)
(MORE TBC)
STEERING COMMITTEE
Samson Abramsky, Anuj Dawar, Juliette Kennedy, Ulrich Kohlenbach, Daniel
Leivant, Leonid Libkin, Lawrence Moss, Luke Ong, Valeria de Paiva, Ruy de
Queiroz, Alexandra Silva, Renata Wassermann.
ADVISORY COMMITTEE
Johan van Benthem, Joe Halpern, Wilfrid Hodges, Angus Macintyre, Hiroakira
Ono, Jouko Väänänen.
ORGANISING COMMITTEE
Ștefan Ciobâcă (Alexandru Ioan Cuza Univ) (Co-Chair)
(more to be announced)
Anjolina G. de Oliveira (Univ Federal de Pernambuco, Brasil)
Ruy de Queiroz (Univ Federal de Pernambuco, Brasil) (co-chair)
SCIENTIFIC SPONSORSHIP
Interest Group in Pure and Applied Logics (IGPL)
The Association for Logic, Language and Information (FoLLI)
Association for Symbolic Logic (ASL) (tbc)
European Association for Theoretical Computer Science (EATCS) (tbc)
Sociedade Brasileira de Lógica (SBL) (tbc)
SPECIAL SESSION: SCREENING OF MOVIES ABOUT MATHEMATICIANS
It is planned to have a special session with the exhibition of a one-hour
documentary film about a remarkable mathematician who is considered a
father of modern differential geometry. "Taking the Long View: The Life of
Shiing-shen Chern" (George Scisery, 2011) examines the life of a remarkable
mathematician whose formidable mathematical contributions were matched by
an approach and vision that helped build bridges between China and the
West. The biographical documentary follows Shiing-shen Chern (1911-2004)
through many of the most dramatic events of the 20th century, portraying a
man who dedicated his life to pure mathematics with the style of a
classical Chinese sage. (zalafilms.com)
FURTHER INFORMATION
Contact one of the Co-Chairs of the Organising Committee.
WEB PAGE
http://wollic.org/wollic2022/
*******************************************************
* PhD position in Logical Approach to Verification of Hyperproperties
* University of Sheffield, UK
* Fully funded for 3.5 years for students applicable for UK Home rates
* Possible times to start: ASAP/Spring 2022/Autumn 2022
*******************************************************
I am looking for a motivated PhD student to join the Verification group (https://www.sheffield.ac.uk/dcs/research/groups/verification <https://www.sheffield.ac.uk/dcs/research/groups/verification>) of The University of Sheffield (https://www.sheffield.ac.uk/dcs). The topic of the PhD project is quite flexible, but should relate to logical theory of verification (for more details: https://www.jobs.ac.uk/job/CLH126/phd-studentship-logical-approach-to-verif…).
The Studentship will cover tuition fees at the UK rate and provide a tax-free stipend at the standard UKRC rate (currently £15,609 for 2021/22) for three and a half years. International students are eligible to apply, however will have to pay the difference between the UK and Overseas tuition fees.
Interested candidates are encouraged to contact me directly by email for further details (j.t.virtema(a)sheffield.ac <mailto:j.t.virtema@sheffield.ac>.uk). For more details on the topic, the candidate may refer to the subsection “Logics for Verification” at http://www.virtema.fi/ <http://www.virtema.fi/>.
Best wishes,
Jonni
- Application deadline: Midnight, 9 Jan 2022
- Starting date: As soon as possible
- 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/Cornell) and Matteo Sammartino (Royal Holloway University of London).
This is a joint research effort 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/0721-259-R-R
FORMATS 2022: FIRST CALL FOR PAPERS
20th International Conference on Formal Modeling and Analysis of Timed Systems
https://conferences.ncl.ac.uk/formats2022/
12-17 September 2022, Warsaw, Poland
co-located with CONCUR, FMICS and QEST as part of CONFEST 2022
SCOPE & TOPICS
FORMATS (International Conference on Formal Modeling and Analysis of Timed Systems) is an annual conference which aims to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from different disciplines that share interests in the modelling, design and analysis of timed computational systems. The conference aims to attract researchers interested in real-time issues in hardware design, performance analysis, real-time software, scheduling, semantics and verification of real-timed, hybrid and probabilistic systems.
Typical topics include (but are not limited to):
• Foundations and Semantics: Theoretical foundations of timed systems, languages and models (e.g., timed automata, timed Petri nets, hybrid automata, timed process algebra, max-plus algebra, probabilistic models).
• Methods and Tools: Techniques, algorithms, data structures, and software tools for analyzing timed systems and resolving temporal constraints (e.g., scheduling, worst-case execution time analysis,optimization, model checking, testing, constraint solving).
• Applications: Adaptation and specialization of timing technology in application domains in which timing plays an important role (e.g., real-time software, hardware circuits, scheduling in manufacturing and telecommunication, robotics).
New for this year, FORMATS will incorporate a special track on:
• Learning-based and data-driven systems: We particularly encourage papers that exploit synergies between the formal analysis of timed systems and data-driven techniques (such as reinforcement learning or deep learning), or which target application domains where learning is important (such as robotics or autonomous systems).
PAPER SUBMISSION
FORMATS 2022 solicits high-quality papers reporting research results, experience reports and/or tools related to the topics mentioned above. Submitted papers must contain original, unpublished contributions, not submitted for publication elsewhere. The papers should be submitted electronically in PDF, following the Springer LNCS style guidelines. Two categories of papers are invited:
• Regular papers, which should not exceed 15 pages in length
• Short papers, which should not exceed 7 pages in length
Both page limits exclude references, which are not limited in length. If necessary, the paper may be supplemented with a clearly marked appendix, which will be reviewed at the discretion of the program committee. Each paper will undergo a thorough review process. Papers should be submitted electronically via the EasyChair online submission system: https://easychair.org/conferences/?conf=formats2022
ARTIFACT EVALUATION
This year, FORMATS is encouraging authors to submit artifacts where appropriate, for example to demonstrate how to reproduce experimental data in a research paper or to examine the usability and applicability of a software tool. Artifacts will be submitted and evaluated only for papers accepted for publication. These will be evaluated by the Artifact Evaluation Committee and those that are accepted will receive a repeatability badge to be displayed on the first page of the published version.
PUBLICATION AND BEST PAPER AWARD
The proceedings of FORMATS 2022 will be published by Springer in the Lecture Notes in Computer Science series. The best paper of the conference will be awarded the Oded Maler Award in Timed Systems.
IMPORTANT DATES
• Abstract submission: 19 April 2022
• Paper submission: 22 April 2022
• Acceptance notification: 17 June 2022
• Artifact submission deadline: 24 June 2022
• Camera-ready copy deadline: 15 July 2022
• Conference: 12-17 September 2022
CONFEST 2022, which includes FORMATS 2022, is currently planned as a physical, in-person event with support for remote presence for speakers and participants. Depending on the pandemic situation, a decision whether to cancel the physical component of CONFEST or not will be made by the end of June 2022.
For any questions, feel free to contact the program chairs Sergiy Bogomolov (sergiy.bogomolov(a)ncl.ac.uk) and David Parker (d.a.parker(a)cs.bham.ac.uk).
ORGANISATION
Program Chairs
• Sergiy Bogomolov (UK)
• David Parker (UK)
Artifact Evaluation Chairs
• Akshay Rajhans (USA)
• Paolo Zuliani (UK)
Publicity Chair
• Gethin Norman (UK)
Special Track Chair
• Alessandro Abate (UK)
Program Committee
• Alessandro Abate (UK)
• Parosh Aziz Abdulla (Sweden)
• Erika Abraham (Germany)
• Bernhard Aichernig (Austria)
• Nicolas Basset (France)
• Nathalie Bertrand (France)
• Sergiy Bogomolov (co-chair, UK)
• Lei Bu (China)
• Milan Ceska (Czech Republic)
• Thao Dang (France)
• Catalin Dima (France)
• Rayna Dimitrova (Germany)
• Mirco Giacobbe (UK)
• Radu Grosu (Austria)
• Arnd Hartmanns (The Netherlands)
• Hsi-Ming Ho (UK)
• Peter Gjøl Jensen (Denmark)
• Taylor Johnson (USA)
• Sebastian Junges (Netherlands)
• Joost-Pieter Katoen (Germany)
• Sophia Knight (USA)
• Matthieu Martel (France)
• Gethin Norman (UK)
• Miroslav Pajic (USA)
• David Parker (co-chair, UK)
• Igor Potapov (UK)
• Christian Schilling (Denmark)
• Ana Sokolova (Austria)
• Sadegh Soudjani (UK)
• Stavros Tripakis (USA)
• Jana Tumova (Sweden)
• Naijun Zhan (China)
Steering Committee
• Rajeev Alur (USA)
• Eugene Asarin (France)
• Martin Fränzle (chair, Germany)
• Thomas A. Henzinger (Austria)
• Joost-Pieter Katoen (Germany)
• Kim G. Larsen (Denmark)
• Oded Maler (founding chair, France) (1957-2018)
• Pavithra Prabhakar (USA)
• Mariëlle Stoelinga (The Netherlands)
• Wang Yi (Sweden)
von Havelund, Klaus (US 348B) via fm-announcements
NFM 2022 - FOURTH CALL FOR PAPERS
The 14th NASA Formal Methods Symposium
https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fnfm2022.c…
May 24-27, 2022
Pasadena, California, USA
*** EXTENDED SUBMISSION DEADLINE: January 10, 2022 ***
The symposium is planned to be held in person at California Institute of Technology, but potentially transitioning to fully virtual if the COVID situation persists. Virtual presentations will be possible even if the conference is held in-person.
The symposium has NO registration fee for presenting and attending.
IMPORTANT DATES
- Abstract Submission: January 3, 2021 *** extended ***
- Paper Submission: January 10, 2021 *** extended ***
- Paper Notifications: February 28, 2022
- Camera-ready Papers: March 28, 2022
- Symposium: May 24-27, 2022
THEME OF SYMPOSIUM
The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry requires advanced techniques that address these systems' specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems. The focus of the symposium will be on formal/rigorous techniques for software assurance, including their theory, current capabilities and limitations, as well as their potential application to aerospace during all stages of the software life-cycle.
The NASA Formal Methods Symposium is an annual event organized by the NASA Formal Methods (NFM) Research Group, composed of researchers spanning six NASA centers. The organization of NFM 2022 is being led by the Jet Propulsion Laboratory (JPL), located in Pasadena, California.
TOPICS ON INTEREST
Topics of interest include, but are not limited to, the following aspects of formal methods:
Advances in formal methods
- Interactive and automated theorem proving
- SMT and SAT solving
- Model checking
- Static analysis
- Runtime verification
- Automated testing
- Specification languages, textual and graphical
- Refinement
- Code synthesis
- Design for verification and correct-by-design techniques
- Requirements specification and analysis
Integration of formal methods techniques
- Integration of diverse formal methods techniques
- Use of machine learning and probabilistic reasoning techniques in formal methods
- Integration of formal methods into software engineering practices 
- Combination of formal methods with simulation and analysis techniques
- Formal methods and fault tolerance, resilient computing, and self healing systems
- Formal methods and graphical modeling languages such as SysML, UML, MATLAB/Simulink
- Formal methods and autonomy, e.g., verification of systems and languages for planning and scheduling
(PDDL, Plexil, etc.), self-sufficient systems, and fault-tolerant systems.
Formal methods in practice
- Experience reports of application of formal methods on real systems, such as autonomous systems, safety-critical
systems, concurrent and distributed systems, cyber-physical, embedded, and hybrid systems, fault-detection,
diagnostics, and prognostics systems, and human-machine interaction analysis.
- Use of formal methods in systems engineering (including hardware components)
- Use of formal methods in education
- Reports on negative results in the development and the application for formal methods in practice.
- Usability of formal method tools, and their infusion into industrial contexts.
- Challenge problems for future reference by the formal methods community. The formulation of these papers can range
from plain English description of a problem over formal specifications, to specific implementations in a
programming language.
NASA OPEN SOURCE
Courageous authors, who want to delve in open source software being applied in real NASA missions, and find possible connections to and applications of Formal Methods, are invited to visit the open source repositories for the following two frameworks for programming flight software:
- F’ (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fnasa.gith…)
- cFS (https://cfs.gsfc.nasa.gov/)
SUBMISSIONS
There are two categories of submissions:
- Regular papers describing fully developed work and complete results
(maximum 15 pages, excluding references);
- Short papers on tools, experience reports, or work in progress with preliminary results
(maximum 6 pages, excluding references).
Additional appendices can be submitted as supplementary material for reviewing purposes. They will not be included in the proceedings.
All papers must be in English and describe original work that has not been published.
All submissions will be reviewed by at least three members of the Program Committee. Reviewing is Single-blind.
We encourage authors to focus on readability of their submissions.
Papers will appear in the Formal Methods subline of Springer's Lecture Notes in Computer Science (LNCS) and must use LNCS style formatting (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.sprin…);reserved=0). Papers must be submitted in PDF format at the EasyChair submission site:
https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Feasychair…p;reserved=0.
Authors of selected best papers will be invited to submit an extended version to a special issue in Springer's Innovations in Systems and Software Engineering: A NASA Journal (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.sprin…);reserved=0).
ARTIFACTS
Authors are encouraged, but not strictly required, to submit artifacts that support the conclusions of their work (if allowed by their institutions). Artifacts may contain software, mechanized proofs, benchmarks, examples, case studies and data sets. Artifacts will be evaluated by the Program Committee together with the paper.
ORGANIZERS
PC chairs
- Klaus Havelund, JPL, USA
- Jyo Deshmukh, USC, USA
- Ivan Perez, NIA, USA
Application Advisors
- Robert Bocchino, JPL, USA
- John Day, JPL, USA
- Maged Elasaar, JPL, USA
- Amalaye Oyake, Blue Origin, USA
- Nicolas Rouquette, JPL, USA
- Vandi Verma, JPL, USA
Application advisors advise the PC chairs to ensure a strong connection to the problems facing NASA.
Local Organizer
- Richard Murray, Caltech, USA
Scientific Advisor
- Mani Chandy, Caltech, USA
Program Committee
- Aaron Dutle, NASA, USA
- Alessandro Cimatti, Fondazione Bruno Kessler, Italy
- Anastasia Mavridou, SGT Inc. / NASA Ames Research Center, USA
- Anne-Kathrin Schmuck, Max-Planck-Institute for Software Systems, Germany
- Arie Gurfinkel, University of Waterloo, Canada
- Bardh Hoxha, Toyota Research Institute North America, USA
- Bernd Finkbeiner, CISPA Helmholtz Center for Information Security, Germany
- Betty H.C. Cheng, Michigan State University, USA
- Borzoo Bonakdarpour, Michigan State University, USA
- Carolyn Talcott, SRI International, USA
- Chuchu Fan, MIT, USA
- Constance Heitmeyer, Naval Research Laboratory, USA
- Corina Pasareanu, CMU, NASA, KBR, USA
- Cristina Seceleanu, Mälardalen University, Sweden
- Dejan Nickovic, Austrian Institute of Technology AIT, Austria
- Dirk Beyer, LMU Munich, Germany
- Doron Peled, Bar Ilan University, Israel
- Erika Abraham, RWTH Aachen University, Germany
- Ewen Denney, NASA, USA
- Gerard Holzmann, Nimble Research, USA
- Giles Reger, The University of Manchester, UK
- Huafeng Yu, TOYOTA InfoTechnology Center USA, USA
- Jean-Christophe Filliatre, CNRS, France
- Johann Schumann, NASA, USA
- John Day, Jet Propulsion Laboratory, USA
- Julia Badger, NASA, USA
- Julien Signoles, CEA LIST, France
- Kerianne Hobbs, Air Force Research Laboratory, USA
- Kristin Yvonne Rozier, Iowa State University, USA
- Leonardo Mariani, University of Milano Bicocca, Italy
- Lu Feng, University of Virginia, USA
- Marcel Verhoef, European Space Agency, The Netherlands
- Marie Farrell, Maynooth University, Ireland
- Marieke Huisman, University of Twente, The Netherlands
- Marielle Stoelinga, University of Twente, The Netherlands
- Martin Feather, Jet Propulsion Laboratory, USA
- Martin Leucker, University of Luebeck, Germany
- Michael Lowry, NASA, USA
- Misty Davies, NASA, USA
- Natasha Neogi, NASA, USA
- Nicolas Rouquette, Jet Propulsion Laboratory, USA
- Nikos Arechiga, Toyota Research Institute, USA
- Rajeev Joshi, Amazon Web Services, USA
- Stanley Bak, Stony Brook University, USA
- Sylvie Boldo, INRIA, France
- Vandi Verma, NASA, USA
- Willem Visser, Amazon Web Services, USA
CONTACT
Email: nfm2022 [at] easychair [dot] org
---
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