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

Fully funded PhD positions in logic, semantics of programs and

von Jonni T Virtema

** 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, 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 https://www.sheffield.ac.uk/dcs/research/groups/verification <https://www.sheffield.ac.uk/dcs/research/groups/verification> For informal enquiries, please do not hesitate to contact any group member by email. Dr. Jonni Virtema is keen to supervise students in any area of his current research, which relate to the interplay of logic and complexity theory. Current topics include logics and complexity theory related to numerical data, and temporal logics designed to express so-called hyperproperties, which are important in information flow and security. A further emerging topic is to study foundations of neural networks using the machinery of logics and complexity theory related to numerical data. See http://www.virtema.fi/ <http://www.virtema.fi/> for further details. Dr. Harsh Beohar is broadly interested in comparative concurrency semantics and in the interplay of category theory, logic, and semantics. Current topics include expressive modal logics, behavioural equivalence games, synthesising distinguishing/characteristic formulae all at the level of coalgebras. See https://dblp.org/pid/13/7482.html <https://dblp.org/pid/13/7482.html> for an uptodate list of publications. Dr. Mike Stannett is interested in formal verification of physical theories, using Isabelle/HOL to verify first-order special and general relativity. Working with researchers at the Renyi Institute in Budapest he has successfully verified the “No Faster-than-Light Observers” theorem for special relativity; he is now collaborating on a locale-based extension of this proof to cover the corresponding theorem of general relativity. Other topics of interest include extending the Hungarian theories to generate a combined first-order quantum/relativistic theory. See https://scholar.google.com/citations?user=kppqMecAAAAJ <https://scholar.google.com/citations?user=kppqMecAAAAJ> for a list of publications.

1 Jahr, 9 Monate

1
0
0 0

[Vardi-list] How Does Technology Impact Society?

von Scientia/De Lange Conference

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 Jahr, 9 Monate

1
0
0 0

Faculty Positions in Cambridge

von Anuj Dawar

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 Jahr, 9 Monate

1
0
0 0

[Vardi-list] A Special Seminar in Honor's of Dana Scott's 90th

von Moshe Y Vardi

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 Jahr, 9 Monate

1
0
0 0

Faculty positions in Oxford

von Sam Staton

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 Jahr, 9 Monate

1
0
0 0

Fully funded PhD positions in logic, semantics of programs and

von Harsh Beohar

** 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 Jahr, 9 Monate

1
0
0 0

Phd Shcolarship

von Guido Sciavicco

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 Jahr, 9 Monate

1
0
0 0

RAMiCS 2023 - Deadline extension

von Michael Winter

(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 Jahr, 10 Monate

1
0
0 0

Lecturer in Verification, University of Sheffield, UK (deadline:

von Jonni T Virtema

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 Jahr, 10 Monate

1
0
0 0

Postdoc Position on Hardware Verification via Model Learning, Royal

von Sammartino, Matteo

- 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 Jahr, 10 Monate

1
0
0 0

2024

2023

2022

2021

2020

2019

2018

finite-model-theory