August 2021 - finite-model-theory - lists.rwth-aachen.de

TABLEAUX 2021 – Call for Participation. 6-9 September, 2021. Virtual and Birmingham, UK.
by anupamdotdas＠gmail.com 25 Aug '21

25 Aug '21

TABLEAUX 2021 The 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods Online and Birmingham, UK, September 6-9, 2021 https://tableaux2021.org/ GENERAL INFORMATION The 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2021) will be hosted by the University of Birmingham, UK, 6-9 September 2021. It will primarily be a virtual conference, due to ongoing conerns about COVID-19. However it will be possible to attend the conference physically for those who are able to travel to Birmingham and take advantage of a hybrid format. TABLEAUX is the main international conference at which research on all aspects -- theoretical foundations, implementation techniques, systems development and applications -- of tableaux-based reasoning and related methods is presented. The first TABLEAUX conference was held in Lautenbach near Karlsruhe, Germany, in 1992. Since then it has been organised on an annual basis (sometimes as a part of IJCAR). TABLEAUX 2021 will be co-located with the 13th International Symposium on Frontiers of Combining Systems (FroCoS 2021). SCOPE OF CONFERENCE Tableaux and other proof based methods offer convenient and flexible tools for automated reasoning for both classical and non-classical logics. Areas of application include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, teaching, and system diagnosis. Topics of interest include but are not limited to: * tableau methods for classical and non-classical logics (including first-order, higher-order, modal, temporal, description, hybrid, intuitionistic, linear, substructural, fuzzy, relevance and non- monotonic logics) and their proof-theoretic foundations; * sequent, natural deduction, labelled, nested and deep calculi for classical and non-classical logics, as tools for proof search and proof representation; * related methods (SMT, model elimination, model checking, connection methods, resolution, BDDs, translation approaches); * flexible, easily extendable, light-weight methods for theorem proving; novel types of calculi for theorem proving and verification in classical and non-classical logics; * systems, tools, implementations, empirical evaluations and applications (provers, proof assistants, logical frameworks, model checkers, etc.); * implementation techniques (data structures, efficient algorithms, performance measurement, extensibility, etc.); * extensions of tableau procedures with conflict-driven learning; * techniques for proof generation and compact (or humanly readable) proof representation; * theoretical and practical aspects of decision procedures; * applications of automated deduction to mathematics, software development, verification, deductive and temporal databases, knowledge representation, ontologies, fault diagnosis or teaching. We also welcome papers describing applications of tableau procedures to real-world examples. Such papers should be tailored to the TABLEAUX community and should focus on the role of reasoning and on logical aspects of the solution. INVITED SPEAKERS TABLEAUX 2021 will host the following the invited speakers: Michael Benedikt (joint with FroCoS) (University of Oxford, UK). The Strange Career of Interpolation and Definability. Orna Kupferman (Hebrew University, Israel). Rational Synthesis. Revantha Ramanayake (University of Groningen, The Netherlands). The Barter Trade in Structure and Cuts. Greg Restall (University of Melbourne, Australia / University of St Andrews, UK). Comparing Rules for Identity in Sequent Systems and Natural Deduction. Renate Schmidt (joint with FroCoS) (University of Manchester, UK). Forgetting and Subontology Generation for the Medical Ontology SNOMED CT. PROGRAM The program can be found here: https://tableaux2021.org/#program . REGISTRATION TABLEAUX and FroCoS will be entirely free-of-charge to attend, but registration is mandatory to fully engage with the scientific program. The registration form is here: https://forms.gle/DRNBgeRKA4Qbcsws7 If you wish to attend physically, you should indicate it on the registration form. Note that you are able to edit this response in case of change of circumstances. More information about the conference format will be updated here. PROGRAM COMMITTEE Bahareh Afshari (University of Amsterdam, Netherlands, and University of Gothenburg, Sweden) Carlos Areces (Universidad Nacional de Córdoba, Argentina) Arnon Avron (Tel-Aviv University, Israel) Nick Bezhanishvili (University of Amsterdam, Netherlands) Patrick Blackburn (University of Roskilde, Denmark) Serenella Cerrito (Université Paris-Saclay, Univ Evry, France) Kaustuv Chaudhuri (Inria, France) Liron Cohen (Ben-Gurion University, Israel) Anupam Das (University of Birmingham, UK) Stéphane Demri (CNRS, France) Hans de Nivelle (Nazarbayev University, Kazakhstan) Valeria de Paiva (Topos Institute Berkeley, USA) Clare Dixon (University of Manchester, UK) Christian Fermüller (TU Wien, Austria) Didier Galmiche (Université de Lorraine, France) Silvio Ghilardi (Università degli Studi di Milano, Italy) Rajeev Goré (Australian National University, Australia) Andrzej Indrzejczak (University of Łódź, Poland) Hidenori Kurokawa (Kanazawa University, Japan) Stepan Kuznetsov (Russian Academy of Sciences, Russia) Björn Lellmann (SBA Research, Austria) Stéphane Graham-Lengrand (SRI International, USA) George Metcalfe (University of Bern, Switzerland) Neil Murray (University At Albany, USA) Cláudia Nalon (Universidade de Brasília, Brazil) Sara Negri (University of Genoa, Italy) Nicola Olivetti (Aix-Marseille University, France) Eugenio Orlandelli (University of Bologna, Italy) Jens Otten (University of Oslo, Norway) Alessandra Palmigiano (Vrije Universiteit Amsterdam, Netherlands) Dirk Pattinson (Australian National University, Australia) Frank Pfenning (Carnegie Mellon University, USA) Elaine Pimentel (Federal University of Rio Grande do Norte, Brazil) Andrei Popescu (University of Sheffield, UK) Gian Luca Pozzato (University of Turin, Italy) Giselle Reis (Carnegie Mellon University, Qatar) Reuben Rowe (Royal Holloway, UK) José Espírito Santo (University of Minho, Portugal) Lutz Straßburger (Inria, France) Josef Urban (Czech Technical University in Prague, Czech Republic) PC CHAIRS Anupam Das (University of Birmingham, UK) Sara Negri (University of Genoa, Italy)

1 0

[fm-announcements] Certified Programs and Proofs (CPP) 2022: Final Call for Papers
by Titolo, Laura (LARC-D320)[NATIONAL INSTITUTE OF AEROSPACE] via fm-announcements 19 Aug '21

19 Aug '21

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://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fpopl22.si…) will be held on 17-18 January 2022 and will be co-located with POPL 2022 in Philadelphia, Pennsylvania, United States. CPP 2022 is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG. CPP 2022 will welcome contributions from all members of the community. The CPP 2022 organizers will strive to enable both in-person and remote participation, in cooperation with the POPL 2022 organizers. NEWS If the authors of a CPP 2022 accepted paper will be unable or unwilling to travel to the conference, the organizers can confirm that this will not affect the paper’s publication in the proceedings, and the authors will be able to upload recorded talks that will be made publicly available. IMPORTANT DATES * Abstract Submission Deadline: 16 September 2021 at 23:59 AoE (UTC-12h) * Paper Submission Deadline: 22 September 2021 at 23:59 AoE (UTC-12h) * Notification (tentative): 22 November 2021 * Camera Ready Deadline (tentative): 12 December 2021 * Conference: 17-18 January 2022 Deadlines expire at the end of the day, anywhere on earth. Abstract and submission deadlines are strict and there will be no extensions. DISTINGUISHED PAPER AWARDS Around 10% of the accepted papers at CPP 2022 will be designated as Distinguished Papers. This award highlights papers that the CPP program committee thinks should be read by a broad audience due to their relevance, originality, significance and clarity. TOPICS OF INTEREST We welcome submissions in research areas related to formal certification of programs and proofs. The following is a non-exhaustive list of topics of interest to CPP: * certified or certifying programming, compilation, linking, OS kernels, runtime systems, security monitors, and hardware; * certified mathematical libraries and mathematical theorems; * proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL4, HOL Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc); * new languages and tools for certified programming; * program analysis, program verification, and program synthesis; * program logics, type systems, and semantics for certified code; * logics for certifying concurrent and distributed systems; * mechanized metatheory, formalized programming language semantics, and logical frameworks; * higher-order logics, dependent type theory, proof theory, logical systems, separation logics, and logics for security; * verification of correctness and security properties; * formally verified blockchains and smart contracts; * certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; * certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; * certificates for program termination; * formal models of computation; * mechanized (un)decidability and computational complexity proofs; * formally certified methods for induction and coinduction; * integration of interactive and automated provers; * logical foundations of proof assistants; * applications of AI and machine learning to formal certification; * user interfaces for proof assistants and theorem provers; * teaching mathematics and computer science with proof assistants. SUBMISSION GUIDELINES Prior to the paper submission deadline, the authors should upload their anonymized paper in PDF format through the HotCRP system at https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcpp2022.h… The submissions must be written in English and provide sufficient detail to allow the program committee to assess the merits of the contribution. They must be formatted following the ACM SIGPLAN Proceedings format using the acmart style with the sigplan option, which provides a two-column style, using 10 point font for the main text, and a header for double blind review submission, i.e., \documentclass[sigplan,10pt,anonymous,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false} The submitted papers should not exceed 12 pages, including tables and figures, but excluding bibliography and clearly marked appendices. The papers should be self-contained without the appendices. Shorter papers are welcome and will be given equal consideration. Submissions not conforming to the requirements concerning format and maximum length may be rejected without further consideration. CPP 2022 will employ a lightweight double-blind reviewing process. To facilitate this, the submissions must adhere to two rules: (1) author names and institutions must be omitted, and (2) references to authors’ own related work should be in the third person (e.g., not "We build on our previous work ..." but rather "We build on the work of ..."). The purpose of this process is to help the PC and external reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing it more difficult. In particular, important background references should not be omitted or anonymized. In addition, authors are free to disseminate their ideas or draft versions of their papers as usual. For example, authors may post drafts of their papers on the web or give talks on their research ideas. POPL has answers to frequently asked questions addressing many common concerns: https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fpopl20.si… We strongly encourage the authors to provide any supplementary material that supports the claims made in the paper, such as proof scripts or experimental data. This material must be uploaded at submission time, as an archive, not via a URL. Two forms of supplementary material may be submitted: (1) Anonymous supplementary material is made available to the reviewers before they submit their first-draft reviews. (2) Non-anonymous supplementary material is made available to the reviewers after they have submitted their first-draft reviews and have learned the identity of the authors. Please use anonymous supplementary material whenever possible, so that it can be taken into account from the beginning of the reviewing process. The submitted papers must adhere to the SIGPLAN Republication Policy (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.sigpl…) and the ACM Policy on Plagiarism (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.acm.o…). Concurrent submissions to other conferences, journals, workshops with proceedings, or similar forums of publication are not allowed. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. One author of each accepted paper is expected to present it at the (possibly virtual) conference. PUBLICATION, COPYRIGHT AND OPEN ACCESS The CPP 2022 proceedings will be published by the ACM, and authors of accepted papers will be required to choose one of the following publication options: (1) Author retains copyright of the work and grants ACM a non-exclusive permission-to-publish license and, optionally, licenses the work under a Creative Commons license. (2) Author retains copyright of the work and grants ACM an exclusive permission-to-publish license. (3) Author transfers copyright of the work to ACM. For authors who can afford it, we recommend option (1), which will make the paper Gold Open Access, and also encourage such authors to license their work under the CC-BY license. ACM will charge you an article processing fee for this option (currently, US$700), which you have to pay directly with the ACM. For everyone else, we recommend option (2), which is free and allows you to achieve Green Open Access, by uploading a preprint of your paper to a repository that guarantees permanent archival such as arXiv or HAL. This is anyway a good idea for timely dissemination even if you chose option 1. Ensuring timely dissemination is particularly important for this edition, since, because of the very tight schedule, the official proceedings might not be available in time for CPP. The official CPP 2022 proceedings will also be available via SIGPLAN OpenTOC (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.sigpl…). For ACM’s take on this, see their Copyright Policy (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.acm.o…) and Author Rights (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fauthors.a…). PROGRAM COMMITTEE Andrei Popescu, University of Sheffield, United Kingdom (co-chair) Steve Zdancewic, University of Pennsylvania, United States (co-chair) Mohammad Abdulaziz, TU München, Germany Mauricio Ayala-Rincón, Universidade de Brasília, Brazil Andrej Bauer, University of Ljubljana, Slovenia Thomas Bauereiss, University of Cambridge, United Kingdom Yves Bertot, Inria and Université Cote d'Azur, France Lars Birkedal, Aarhus University, Denmark Sylvie Boldo, Inria and Université Paris-Saclay, France Qinxiang Cao, Shanghai Jiao Tong University, China Évelyne Contejean, Laboratoire Méthodes Formelles, CNRS, France Benjamin Delaware, Purdue University, United States Simon Foster, University of York, United Kingdom Alwyn Goodloe, NASA Langley Research Center, United States Armaël Guéneau, Aarhus University, Denmark John Harrison, Amazon Web Services, United States Joe Hendrix, Galois, Inc, United States Aquinas Hobor, National University of Singapore, Singapore Ralf Jung, MPI-SWS, Germany Cezary Kaliszyk, University of Innsbruck, Austria Jeehoon Kang, KAIST, South Korea Hongjin Liang, Nanjing University, China Gregory Malecha, BedRock Systems, Inc, United States Anders Mörtberg, Stockholm University, Sweden Toby Murray, University of Melbourne, Australia Zoe Paraskevopoulou , Northeastern University, United States Brigitte Pientka, McGill University, Canada Aseem Rastogi, Microsoft Research, India Bas Spitters, Aarhus University, Denmark Kathrin Stark, Princeton University, United States Hira Taqdees Syeda, Chalmers University of Technology, Sweden Joseph Tassarotti, Boston College, United States Laura Titolo, NIA/NASA LaRC, United States Sophie Tourret, Inria, France Dmitriy Traytel, University of Copenhagen, Denmark Floris van Doorn, Paris-Saclay University, France Freek Verbeek, Open University of The Netherlands, Netherlands Freek Wiedijk, Radboud Universiteit Nijmegen, Netherlands ORGANIZERS Lennart Beringer, Princeton University, United States (conference co-chair) Robbert Krebbers, Radboud University, Netherlands (conference co-chair) Andrei Popescu, University of Sheffield, United Kingdom (PC co-chair) Steve Zdancewic, University of Pennsylvania, United States (PC co-chair) CONTACT For any questions please contact the two PC chairs: Andrei Popescu <mailto:a.popescu@sheffield.ac.uk> Steve Zdancewic <mailto:stevez@seas.upenn.edu> --- 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

1 0

Certified Programs and Proofs (CPP) 2022: Final Call for Papers
by Andrei Popescu 19 Aug '21

19 Aug '21

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 in Philadelphia, Pennsylvania, United States. CPP 2022 is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG. CPP 2022 will welcome contributions from all members of the community. The CPP 2022 organizers will strive to enable both in-person and remote participation, in cooperation with the POPL 2022 organizers. NEWS If the authors of a CPP 2022 accepted paper will be unable or unwilling to travel to the conference, the organizers can confirm that this will not affect the paper’s publication in the proceedings, and the authors will be able to upload recorded talks that will be made publicly available. IMPORTANT DATES * Abstract Submission Deadline: 16 September 2021 at 23:59 AoE (UTC-12h) * Paper Submission Deadline: 22 September 2021 at 23:59 AoE (UTC-12h) * Notification (tentative): 22 November 2021 * Camera Ready Deadline (tentative): 12 December 2021 * Conference: 17-18 January 2022 Deadlines expire at the end of the day, anywhere on earth. Abstract and submission deadlines are strict and there will be no extensions. DISTINGUISHED PAPER AWARDS Around 10% of the accepted papers at CPP 2022 will be designated as Distinguished Papers. This award highlights papers that the CPP program committee thinks should be read by a broad audience due to their relevance, originality, significance and clarity. TOPICS OF INTEREST We welcome submissions in research areas related to formal certification of programs and proofs. The following is a non-exhaustive list of topics of interest to CPP: * certified or certifying programming, compilation, linking, OS kernels, runtime systems, security monitors, and hardware; * certified mathematical libraries and mathematical theorems; * proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL4, HOL Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc); * new languages and tools for certified programming; * program analysis, program verification, and program synthesis; * program logics, type systems, and semantics for certified code; * logics for certifying concurrent and distributed systems; * mechanized metatheory, formalized programming language semantics, and logical frameworks; * higher-order logics, dependent type theory, proof theory, logical systems, separation logics, and logics for security; * verification of correctness and security properties; * formally verified blockchains and smart contracts; * certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; * certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; * certificates for program termination; * formal models of computation; * mechanized (un)decidability and computational complexity proofs; * formally certified methods for induction and coinduction; * integration of interactive and automated provers; * logical foundations of proof assistants; * applications of AI and machine learning to formal certification; * user interfaces for proof assistants and theorem provers; * teaching mathematics and computer science with proof assistants. SUBMISSION GUIDELINES Prior to the paper submission deadline, the authors should upload their anonymized paper in PDF format through the HotCRP system at https://cpp2022.hotcrp.com The submissions must be written in English and provide sufficient detail to allow the program committee to assess the merits of the contribution. They must be formatted following the ACM SIGPLAN Proceedings format using the acmart style with the sigplan option, which provides a two-column style, using 10 point font for the main text, and a header for double blind review submission, i.e., \documentclass[sigplan,10pt,anonymous,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false} The submitted papers should not exceed 12 pages, including tables and figures, but excluding bibliography and clearly marked appendices. The papers should be self-contained without the appendices. Shorter papers are welcome and will be given equal consideration. Submissions not conforming to the requirements concerning format and maximum length may be rejected without further consideration. CPP 2022 will employ a lightweight double-blind reviewing process. To facilitate this, the submissions must adhere to two rules: (1) author names and institutions must be omitted, and (2) references to authors’ own related work should be in the third person (e.g., not "We build on our previous work ..." but rather "We build on the work of ..."). The purpose of this process is to help the PC and external reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing it more difficult. In particular, important background references should not be omitted or anonymized. In addition, authors are free to disseminate their ideas or draft versions of their papers as usual. For example, authors may post drafts of their papers on the web or give talks on their research ideas. POPL has answers to frequently asked questions addressing many common concerns: https://popl20.sigplan.org/track/POPL-2020-Research-Papers#Submission-and-R… We strongly encourage the authors to provide any supplementary material that supports the claims made in the paper, such as proof scripts or experimental data. This material must be uploaded at submission time, as an archive, not via a URL. Two forms of supplementary material may be submitted: (1) Anonymous supplementary material is made available to the reviewers before they submit their first-draft reviews. (2) Non-anonymous supplementary material is made available to the reviewers after they have submitted their first-draft reviews and have learned the identity of the authors. Please use anonymous supplementary material whenever possible, so that it can be taken into account from the beginning of the reviewing process. The submitted papers must adhere to the SIGPLAN Republication Policy (https://www.sigplan.org/Resources/Policies/Republication/) and the ACM Policy on Plagiarism (https://www.acm.org/publications/policies/plagiarism). Concurrent submissions to other conferences, journals, workshops with proceedings, or similar forums of publication are not allowed. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. One author of each accepted paper is expected to present it at the (possibly virtual) conference. PUBLICATION, COPYRIGHT AND OPEN ACCESS The CPP 2022 proceedings will be published by the ACM, and authors of accepted papers will be required to choose one of the following publication options: (1) Author retains copyright of the work and grants ACM a non-exclusive permission-to-publish license and, optionally, licenses the work under a Creative Commons license. (2) Author retains copyright of the work and grants ACM an exclusive permission-to-publish license. (3) Author transfers copyright of the work to ACM. For authors who can afford it, we recommend option (1), which will make the paper Gold Open Access, and also encourage such authors to license their work under the CC-BY license. ACM will charge you an article processing fee for this option (currently, US$700), which you have to pay directly with the ACM. For everyone else, we recommend option (2), which is free and allows you to achieve Green Open Access, by uploading a preprint of your paper to a repository that guarantees permanent archival such as arXiv or HAL. This is anyway a good idea for timely dissemination even if you chose option 1. Ensuring timely dissemination is particularly important for this edition, since, because of the very tight schedule, the official proceedings might not be available in time for CPP. The official CPP 2022 proceedings will also be available via SIGPLAN OpenTOC (http://www.sigplan.org/OpenTOC/#cpp). For ACM’s take on this, see their Copyright Policy (http://www.acm.org/publications/policies/copyright-policy) and Author Rights (http://authors.acm.org/main.html). PROGRAM COMMITTEE Andrei Popescu, University of Sheffield, United Kingdom (co-chair) Steve Zdancewic, University of Pennsylvania, United States (co-chair) Mohammad Abdulaziz, TU München, Germany Mauricio Ayala-Rincón, Universidade de Brasília, Brazil Andrej Bauer, University of Ljubljana, Slovenia Thomas Bauereiss, University of Cambridge, United Kingdom Yves Bertot, Inria and Université Cote d'Azur, France Lars Birkedal, Aarhus University, Denmark Sylvie Boldo, Inria and Université Paris-Saclay, France Qinxiang Cao, Shanghai Jiao Tong University, China Évelyne Contejean, Laboratoire Méthodes Formelles, CNRS, France Benjamin Delaware, Purdue University, United States Simon Foster, University of York, United Kingdom Alwyn Goodloe, NASA Langley Research Center, United States Armaël Guéneau, Aarhus University, Denmark John Harrison, Amazon Web Services, United States Joe Hendrix, Galois, Inc, United States Aquinas Hobor, National University of Singapore, Singapore Ralf Jung, MPI-SWS, Germany Cezary Kaliszyk, University of Innsbruck, Austria Jeehoon Kang, KAIST, South Korea Hongjin Liang, Nanjing University, China Gregory Malecha, BedRock Systems, Inc, United States Anders Mörtberg, Stockholm University, Sweden Toby Murray, University of Melbourne, Australia Zoe Paraskevopoulou , Northeastern University, United States Brigitte Pientka, McGill University, Canada Aseem Rastogi, Microsoft Research, India Bas Spitters, Aarhus University, Denmark Kathrin Stark, Princeton University, United States Hira Taqdees Syeda, Chalmers University of Technology, Sweden Joseph Tassarotti, Boston College, United States Laura Titolo, NIA/NASA LaRC, United States Sophie Tourret, Inria, France Dmitriy Traytel, University of Copenhagen, Denmark Floris van Doorn, Paris-Saclay University, France Freek Verbeek, Open University of The Netherlands, Netherlands Freek Wiedijk, Radboud Universiteit Nijmegen, Netherlands ORGANIZERS Lennart Beringer, Princeton University, United States (conference co-chair) Robbert Krebbers, Radboud University, Netherlands (conference co-chair) Andrei Popescu, University of Sheffield, United Kingdom (PC co-chair) Steve Zdancewic, University of Pennsylvania, United States (PC co-chair) CONTACT For any questions please contact the two PC chairs: Andrei Popescu <a.popescu(a)sheffield.ac.uk> Steve Zdancewic <stevez(a)seas.upenn.edu>

1 0

[fm-announcements] [FMICS 2021] Call for Participation
by Perez Dominguez, Ivan (LARC-D320)[NATIONAL INSTITUTE OF AEROSPACE] via fm-announcements 18 Aug '21

18 Aug '21

**************************************************************** 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

1 0

Logica Universalis Webinar - August 18 - Logical constants in abstract frameworks and A Note on Logicality of Generalized Quantifiers by Tin Perkov
by Antje Herbst 16 Aug '21

16 Aug '21

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

1 0

Yale Weiss / Saul Kripke Center / Mel Fitting / LUWebinar today at 16 pm CET
by jean-yves beziau 11 Aug '21

11 Aug '21

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

1 0

PhD positions in Computer Science and Artificial Intelligence at DISI - University of Trento
by Marco Roveri 10 Aug '21

10 Aug '21

1 0

Logica Universalis Webinar - August 11 - A Reinterpretation of the Semilattice Semantics with Applications by Yale Weiss
by Antje Herbst 10 Aug '21

10 Aug '21

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

1 0