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

[Vardi-list] How Does Technology Impact Society?
by Scientia/De Lange Conference 08 Oct '22

08 Oct '22

View this email in your browser (https://urldefense.com/v3/__https://mailchi.mp/605dde346bbc/technology-cult… ) Don’t miss the opportunity to save! Early bird registration deadline ends October 17! REGISTER TODAY (https://urldefense.com/v3/__https://rice.us20.list-manage.com/track/click?u… ) This conference will focus on the exploration of the dynamic interaction between technology, society, and culture. More specifically, the conference will address the challenges of information technology, health and medicine, and climate change (https://urldefense.com/v3/__https://rice.us20.list-manage.com/track/click?u… ) from the three perspectives of technology, culture and society. More information is available at delange.rice.edu. (https://urldefense.com/v3/__https://rice.us20.list-manage.com/track/click?u… ) CALL FOR POSTERS (https://urldefense.com/v3/__https://rice.us20.list-manage.com/track/click?u… ) This email was sent to vardi(a)cs.rice.edu (mailto:vardi@cs.rice.edu) why did I get this? (https://urldefense.com/v3/__https://rice.us20.list-manage.com/about?u=5547a… ) unsubscribe from this list (https://urldefense.com/v3/__https://rice.us20.list-manage.com/unsubscribe?u… ) update subscription preferences (https://urldefense.com/v3/__https://rice.us20.list-manage.com/profile?u=554… ) Rice University Scientia Institute/ De Lange Conference . 6100 Main St . Houston, TX 77005-1827 . USA Email Marketing Powered by Mailchimp https://urldefense.com/v3/__http://www.mailchimp.com/email-referral/?utm_so… _______________________________________________ Vardi-list mailing list Vardi-list(a)mailman.rice.edu https://mailman.rice.edu/mailman/listinfo/vardi-list

1 0

Faculty Positions in Cambridge
by Anuj Dawar 07 Oct '22

07 Oct '22

The Department of Computer Science and Technology at the University of Cambridge is currently advertising a number of new faculty positions. These include a position in the area of Algorithms and Complexity: https://www.jobs.cam.ac.uk/job/37368/ and a position in Logical Foundations and Formal Methods: https://www.jobs.cam.ac.uk/job/37369/ which may be of interest to readers of this list. -- Anuj.Dawar(a)cl.cam.ac.uk Professor of Logic and Algorithms Department of Computer Science and Technology University of Cambridge Phone: +44 1223 334408 15 J.J. Thomson Avenue Fax: +44 1223 334678 Cambridge CB3 0FD, UK. http://www.cst.cam.ac.uk/people/ad260

1 0

[Vardi-list] A Special Seminar in Honor's of Dana Scott's 90th
by Moshe Y Vardi 07 Oct '22

07 Oct '22

On Tuesday, October 11th, we'll be celebrating Dana Scott's 90th birthday with a special seminar by Gordon Plotkin, titled "Does recursion help?". The seminar will be held both online and in person at the Topos Institute's Berkeley office, with Gordon and Dana both present in person. Dana will say some opening words before Gordon's talk. An abstract for Gordon's talk, and links to join via Zoom or YouTube livestream, are below. If you would like to attend in person, please email juliet(a)topos.institute to register as a visitor. See https://topos.site/berkeley-seminar/ ---------------------------------------------------------------------------- Date: Tuesday October 11th, 2022 Time: 1700 UTC (10am Berkeley time) Zoom Link: https://topos-institute.zoom.us/j/87874851972?pwd=eWRjZlUvQWJoNmJFdHgycE1mU… Password: happybday YouTube stream: https://youtu.be/n7moEQtv3qU -- Title: Does recursion help? Speaker: Gordon Plotkin Abstract: As everyone knows, Alonzo Church proposed that the effectively calculable natural number functions are those definable in the untyped lambda calculus. (He used Church numerals to represent natural numbers.) The lambda-definable functions were shown to be the same as the Gödel-Herbrand general recursive functions and the same as the functions computable by Turing machines. The fixed-point combinator Y is crucial for the proofs, as it enables functions to be defined recursively. If we switch to the typed lambda-calculus the situation changes drastically. Helmut Schwichtenberg and Richard Statman showed that only the extended polynomials can then be defined (they used a typed version of the Church numerals). It is natural, therefore, to ask what happens if one adds typed fixed-point combinators to the typed lambda calculus. We present an answer to this question. Our answer makes essential use of Dana Scott's domain theory to model the fixed-point combinators. _______________________________________________ Vardi-list mailing list Vardi-list(a)mailman.rice.edu https://mailman.rice.edu/mailman/listinfo/vardi-list

1 0

Faculty positions in Oxford
by Sam Staton 02 Oct '22

02 Oct '22

The Computer Science Department at the University of Oxford is hiring four new faculty. The positions are open to all areas of computer science. The closing date is 12 noon on 14 December 2022. For more information, see https://www.cs.ox.ac.uk/aboutus/vacancies/vacancy-faculty-hiring.html Thanks, Sam.

1 0

Fully funded PhD positions in logic, semantics of programs and
by Harsh Beohar 29 Sep '22

29 Sep '22

** Apologies if you receive multiple copies of these open positions ** Up to three fully funded research and teaching assistant positions with the opportunity of undertaking a PhD are available within the Verification Group, Department of Computer Science, at the University of Sheffield: *https://www.sheffield.ac.uk/dcs/research/groups/verification <https://www.sheffield.ac.uk/dcs/research/groups/verification>* The verification group at Sheffield is growing rapidly. These posts provide excellent opportunities for graduate students (UK and overseas) to obtain a PhD in any active research area of the group, including semantics of concurrent and distributed systems, logics and complexity, algebraic and categorical approaches to program semantics, coalgebras, verification of multi-core programs and weak memory models, interactive theorem proving. The posts are fully funded for 6 years with 60% devoted to research and 40% to teaching support. For more detailed information (including roles and responsibilities), please see: https://www.jobs.ac.uk/job/CTM862/teaching-and-research-assistant-in-comput… For details on possible supervisors and research projects, please contact our personal websites from our group webpage. For informal enquiries, please do not hesitate to contact any group member by email. The candidates interested in the interplay of category theory (coalgebras), logic, and semantics can write directly to me at h.beohar(a)sheffield.ac.uk. Current topics include expressive modal logics, behavioural equivalence games, synthesising distinguishing/characteristic formulae all at the level of coalgebras. With kind regards, Harsh Beohar

1 0

Phd Shcolarship
by Guido Sciavicco 28 Sep '22

28 Sep '22

PhD opportunity The University of Ferrara offers a PhD scholarship officially branded as 'PhD in Mathematics', but, in fact, in Computer Science, within the context of the co-joined PhD program of the universities of Ferrara, Modena, and Parma (Italy, Emilia-Romagna region). The program is three-years long, at the end of which a thesis must be produced. In this case, the scholarship is co-funded by an international company, and the work will be theoretical-practical in every aspect. The gross salary is around 16000 euros/year, but with a very convenient tax schema, that leaves the net salary around 1100 euro/month. The candidate will work in the context of the ACLAI lab at the University of Ferrara (https://aclai.unife.it/) and this scholarship is about bio-sensors applied to emergency/rescue operators, their signals, their wearability, and -top-down as well as AI-based- systems to detect dangerous situations in single operators. In the context of the PhD, the candidate will be expected to produce theoretical research as well as participate in the real implementation of such systems. Under the assumption of a successful program with satisfaction from all parties, the company is prepared to offer a permanent working contract at the end of the PhD, with a salary to be discussed. The ultimate deadline to apply is 11th of October. Please refer to prof. Guido Sciavicco (guido.sciavicco(a)unife.it) for all enquiries; an informal online interview will be necessary prior the application, and applicants must be informed that, in case of winning the public competition, an immediate relocation of the candidate is expected.

1 0

RAMiCS 2023 - Deadline extension
by Michael Winter 23 Sep '22

23 Sep '22

(Apologies for multiple posting) RAMICS DEADLINE EXTENDED 20th International Conference on Relational and Algebraic Methods in Computer Science RAMiCS 2023 3 to 6 April 2023, Technologiezentrum Augsburg, Germany https://ramics20.lis-lab.fr/ IMPORTANT DATES: Abstract Submission (extended): October 7, 2022 Paper Submission (extended): October 14, 2022 Author Notification: December 16, 2022 Final Version: January 06, 2023 RAMiCS 2023: April 03-06, 2023 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. RAMiCS 2023 will take place at the Technologiezentrum Augsburg. Depending on the Covid-19 situation, it will take the form of a physical conference, a virtual conference, or a hybrid between the two. TOPICS: We invite 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 INVITED SPEAKERS Alexander Knapp, Augsburg University, Germany John Stell, University of Leeds, UK Valeria Vignudelli, CNRS/ENS Lyon, France SUBMISSION INSTRUCTIONS: Submission is via EasyChair at https://www.easychair.org/conferences/?conf=ramics2023 All papers will be peer-reviewed by at least three referees. The proceedings will be published in an LNCS volume by Springer, ready at the conference. Submissions must not be published or under review for publication elsewhere. Submissions must be in English using a PDF not exceeding 16 pages in LNCS style. Submissions must provide sufficient information to judge their merits. Additional material may be provided in a clearly marked appendix or by a reference to a manuscript on a web site. Experimental data, software or mathematical components for theorem provers must be available in sufficient detail for referees. Deviation from these requirements may lead to rejection. One author of each accepted paper is expected to present the paper at the conference. Accepted papers must be produced with LaTeX. Formatting instructions and LNCS style files are available at http://www.springer.de/comp/lncs/authors.html As for earlier RAMiCS conferences, we intend to publish a journal special issue with revised and extended versions of a selection of the best papers. COMMITTEES: Organising Committee -------------------- Conf. & PC Co-Chair: Roland Glück, Deutsches Zentrum für Luft- und Raumfahrt, Germany Conf. & PC Co-Chair: Luigi Santocanale, LIS, Aix-Marseille University, France Conf. & PC Co-Chair: Michael Winter, Brock University, Canada Programme Committee ------------------- Adriana Balan, University Politechnic of Bucharest, Romania Manuel Bodirsky, Technical University Dresden, Germany Paul Brunet, Paris-East Créteil University, France Miguel Couceiro, Loria, Nancy, France Manfred Droste, Leipzig University, Germany Uli Fahrenberg, Epita, France Hitoshi Furusawa, Kagoshima University, Japan Wesley Fussner, University of Bern, Switzerland Silvio Ghilardi, University of Milan, Italy Roland Glueck, German Aerospace Center, Augsburg, Germany Walter Guttmann, University of Canterbury, New Zealand Robin Hirsch, University College London, UK Peter Höfner, Australian National University, Canberra, Australia Marcel Jackson, La Trobe University, Melbourne, Australia Ali Jaoua, Qatar University, Qatar Peter Jipsen, Chapman University, Orange, USA Sebastian Joosten, Dartmouth College, Hanover, USA Barbara König, University of Duisburg/Essen, Germany Wendy MacCaull, St. Francis Xavier University, Antigonish, Canada Roger Maddux, Iowa State University, Ames, USA Nelma Moreira, University of Porto, Portugal Martin Mueller, University of Applied Sciences, Bonn-Rhein-Sieg, Germany Damien Pous, CNRS, ENS Lyon, France Luigi Santocanale, Aix-Marseille University, France Ana Sokolova, University of Salzburg, Austria Sara Ugolini, Artificial Intelligence Research Institute of the CSIC, Spain Michael Winter, Brock University, St. Catharines, Canada Sam van Gool, University Paris, France

1 0

Lecturer in Verification, University of Sheffield, UK (deadline:
by Jonni T Virtema 20 Sep '22

20 Sep '22

This is an exciting opportunity for a Lecturer in Verification at the University of Sheffield, a world top 100 University. We are seeking candidates with an outstanding record of scholarship in the logical and mathematical foundations of computing, including 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 of the group 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 that broadly on foundational aspects of computer science. More details: https://www.jobs.ac.uk/job/CTB680/lecturer-in-verification

1 0

Postdoc Position on Hardware Verification via Model Learning, Royal
by Sammartino, Matteo 16 Sep '22

16 Sep '22

- Application deadline: Midnight, 15 Oct 2022 - Salary: £37,467 - Duration: until November 2023 Applications are invited for the post of Post-Doctoral Research Assistant in the Computer Science Department at Royal Holloway, University of London. The post holder will have an exciting opportunity to work on the EPSRC-funded "Verification of Hardware Concurrency via Model Learning" (CLeVer) project (EP/S028641/1), led by Prof. Alexandra Silva (UCL/Cornell) and Matteo Sammartino (RHUL), in collaboration with 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. # Brief description of the project Digital devices are increasingly complex, therefore there is a pressing need to automate the assessment of their correctness. 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 project aims to develop a novel verification framework for hardware, which combines learning, testing and model-checking. Not all models are suitable for this purpose and hence specific classes of models will need to be developed, depending on the task at hand. Subsequently, learning and verification techniques for these classes need to be devised and tested in realistic case studies. We have an industrial partner, ARM, that will provide valuable guidance on the design and development of the aforementioned tasks. # The ideal candidate We are looking for candidates with a PhD in one of the following areas: model-based testing and verification, model learning, 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/0922-411 ============================== Matteo Sammartino, Lecturer Royal Holloway University of London Department of Computer Science Tel.: (+44) (0) 1784 44 3690 Office: 2-07, Bedford Building https://matteosammartino.com/ This email, its contents and any attachments are intended solely for the addressee and may contain confidential information. In certain circumstances, it may also be subject to legal privilege. Any unauthorised use, disclosure, or copying is not permitted. If you have received this email in error, please notify us and immediately and permanently delete it. Any views or opinions expressed in personal emails are solely those of the author and do not necessarily represent those of Royal Holloway, University of London. It is your responsibility to ensure that this email and any attachments are virus free.

1 0

[OVERLAY] Overlay 2022: Call for Papers
by Luca Geatti 12 Sep '22

12 Sep '22

*** We apologize for possible cross posting *** *********** CALL FOR PAPER *********** OVERLAY 2022 28th November - 4th December, 2022 (the precise day(s) will be announced later) Udine, Italy (unless held online, depending on the pandemic emergency situation) https://overlay.uniud.it/workshop/2022 Co-located with AIxIA 2022 https://aixia2022.uniud.it *********** *********** *********** The increasing adoption of Artificial Intelligence techniques in safety-critical systems, employed in real world scenarios, requires the design of reliable, robust, and verifiable methodologies. Artificial Intelligence systems employed in such applications need to provide formal guarantees about their safety, increasing the need for a close interaction between the Artificial Intelligence and Formal Methods scientific communities. To witness this increasing need, tools and methodologies integrating Formal Methods and Artificial Intelligence solutions are getting more and more attention. The workshop is the main official initiative supported by the OVERLAY group (https://overlay.uniud.it). The event aims at establishing a stable, long-term scientific forum on relevant topics connected to the relationships between Artificial Intelligence and Formal Methods, by providing a stimulating environment where researchers can discuss about opportunities and challenges at the border of the two areas. Important goals of the workshop are (i) to encourage the ongoing interaction between the formal methods and artificial intelligence communities, (ii) to identify innovative tools and methodologies, and (iii) to elicit a discussion on open issues and new challenges. This year edition will be held between 28th November and 4th December 2022 (the precise day(s) will be announced later), as a hybrid workshop co-located with AIxIA 2022 (https://aixia2022.uniud.it), which is scheduled to be held in Udine, Italy (unless it will be an online event, depending on the pandemic emergency situation). *** Invited speaker *** Luca Bortolussi (University of Trieste, Italy) *** Call for contributions *** We accept extended abstracts (4 pages + references) focusing on the interaction between Artificial Intelligence and Formal Methods. Invited talks will complement the presentations of contributed papers. Topics of interest include (but are not limited to): automata theory automated reasoning automated planning and scheduling controller synthesis formal specification languages formal verification game theory hybrid and discrete systems logics in computer science reactive synthesis runtime verification and monitoring specification and verification of machine learning systems tools and applications Contributed papers can present recent results at the border of the two fields, new research directions, challenges and perspectives. Presentation of results recently published in other scientific journals or conferences is also welcome. We plan on including all papers in the Proceedings of the event, published at CEUR Workshop Proceedings. CEUR WS proceedings are archival proceedings indexed by DBLP and Scopus. Submitted papers should not exceed four (4) pages plus references. Authors are asked to use CEUR's LaTeX style, available at http://ceur-ws.org/Vol-XXX/CEURART.zip. Submissions must be in PDF format and will be handled via the EasyChair Conference system at the following address: https://easychair.org/conferences/?conf=overlay22. *** Important dates *** - Paper submission: September 30th, 2022 - Acceptance notification: October 21th, 2022 - Camera-ready submission: November 4th, 2022 - Workshop: between 28th November and 4th December, 2022 (the precise day(s) will be announced later) *** COVID-19 Information *** Taking into account the emergency situation, the organizers of OVERLAY 2022 will closely monitor the evolution of the pandemic and will take all the necessary actions to guarantee a successful event. OVERLAY 2022 will be planned as a fully in-person conference, with the possibility, on a limited basis, of participating virtually, if necessary. Should the situation worsen and an in-person event become impossible, OVERLAY 2022 will be transformed into a fully virtual conference. Updates on the organization mode will be published and advertised in due time. In any case, OVERLAY 2022 will be a no-fee event. *** Program Committee *** Chairs Guido Sciavicco - Università di Ferrara Luca Geatti - Free University of Bozen-Bolzano Alessandro Umbrico - ISTC-CNR, Roma PC Members Riccardo De Benedictis, CNR - Institute of Cognitive Sciences and Technologies (CNR-ISTC), Italy Davide Bresolin, University of Padova, Italy Marco Esposito, Sapienza University of Rome, Italy Francesco Fabiano, University of Parma, Italy Marco Gavanelli, University of Parma, Italy Alessandro Gianola, Free University of Bozen-Bolzano, Italy Nicola Gigante, Free University of Bozen-Bolzano, Italy Federico Mari, University of Rome Foro Italico, Italy Andrea Micheli, Fondazione Bruno Kessler, Italy Emilio Munoz-Velasco, University of Malaga, Spain Adriano Peron, University of Naples Federico II, Italy Raine Ronnholm, University of Tampere, Finland Enrico Scala, University of Brescia, Italy Mauro Vallati, University of Huddersfield, United Kingdom Martin Zimmermann, Aalborg University, Denmark *** Contacts *** For more information email overlay2022(a)easychair.org<https://mailto:overlay2022@easychair.org>.

1 0