[TYPES/announce] PhD Position in Deductive Verification of Safety-Critical Software
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Theoretical Computer Science Group at KTH Royal Institute of Technology invites applications for a PhD position in Computer Science focusing on Deductive Verification of Safety-Critical Embedded Software. The doctoral position is within a collaboration project between KTH and Scania, and addresses the need for functional safety of embedded vehicle software. The project relies on formal verification techniques, such as deductive software verification and model checking. The two main problems that the project aims to solve are the problem of connecting, in a formal way, requirements at different systems levels, and the problem of automating the verification process. The first problem will be addressed by the development of a formal framework and tool for hierarchical software architecture modelling that encompasses the given requirements. The second problem will be addressed by the development of automated techniques and tools that read architectural specifications and, from these, automatically generate models and logical specifications for back-end verification tools. This is a five-year full-time employed position involving 20% teaching. We are looking for strong candidates with background in Computer Science, ideally in Formal Methods based on Mathematical Logic and Programming Language Semantics. Industrial experience, especially with embedded safety-critical software, would be an advantage. See https://urldefense.com/v3/__https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:441687/type:job/where:4/apply:1__;!!IBzWLUs!CaZK8Iz_OTSw7EBWjoHj3qF1c8MpRo4eGrCUiu7xB-HqCGMKsspD8BMzXZW3uoqpFXHMPqSGMXWcXw$ for the full announcement with more information and instructions on how to apply. The application deadline is December 6, 2021. Informal enquiries may be sent to dil...@kth.se. Dilian Gurov, Associate Professor School of Electrical Engineering and Computer Science KTH Royal Institute of Technology https://urldefense.com/v3/__https://www.csc.kth.se/*dilian/__;fg!!IBzWLUs!CaZK8Iz_OTSw7EBWjoHj3qF1c8MpRo4eGrCUiu7xB-HqCGMKsspD8BMzXZW3uoqpFXHMPqRvjKiF8w$
[TYPES/announce] PostDoc in Verification of Simulink Models
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] KTH is hiring one PostDoc in Verification of Simulink Models: https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:265239/where:4/ Application deadline: May 16, 2019. Starting date: August 1, 2019 (or by agreement). The postdoctoral position is within a collaboration project between KTH and Scania, and addresses the need for functional safety of embedded vehicle software. The project relies on formal verification techniques, such as deductive software verification and model checking. The two main problems that the project aims to solve are the problem of connecting, in a formal way, requirements at different systems levels, and the problem of automating the verification process. The first problem will be addressed by the development of a formal framework and tool for hierarchical software architecture modelling that encompasses the given requirements. The second problem will be addressed by the development of automated techniques and tools that read architectural specifications and, from these, automatically generate models and logical specifications for back-end verification tools. The postdoc will be responsible for developing a model-checking based automatic verification technique for the exhaustive and systematic verification of C modules developed by means of Simulink models. The main challenge here is to cope with the size and complexity of the industrial Simulink models, that is, to find a technique that can be employed for verification of intricate Simulink models with large state spaces. The position is a full-time research position for one year. Qualifications: Applicants must hold or be about to receive a doctoral degree in Computer Science (or equivalent). The doctoral degree must have been obtained within the last three years from the application deadline (some exceptions for special grounds, for instance sick leave and parental leave). The candidate should have a strong background in Computer Science, and in particular in Formal Methods based on mathematical logic and models of program behavior. Industrial experience, especially with Simulink and embedded safety-critical software, is an advantage. About KTH: KTH Royal Institute of Technology in Stockholm has grown to become one of Europe’s leading technical and engineering universities, as well as a key centre of intellectual talent and innovation. We are Sweden’s largest technical research and learning institution and home to students, researchers and faculty from around the world.
[TYPES/announce] PhD Position in Deductive Verification of Safety-Critical Embedded Software
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Theoretical Computer Science Group at KTH Royal Institute of Technology invites applications for a PhD position in Computer Science focusing on Deductive Verification of Safety-Critical Embedded Software. The doctoral position is within a collaboration project between KTH and Scania, and addresses the need for functional safety of embedded vehicle software. The project relies on formal verification techniques, such as deductive software verification and model checking. The two main problems that the project aims to solve are the problem of connecting, in a formal way, requirements at different systems levels, and the problem of automating the verification process. The first problem will be addressed by the development of a formal framework and tool for hierarchical software architecture modelling that encompasses the given requirements. The second problem will be addressed by the development of automated techniques and tools that read architectural specifications and, from these, automatically generate models and logical specifications for back-end verification tools. This is a five-year full-time employed position involving 20% teaching. We are looking for strong candidates with background in Computer Science, and in particular in Formal Methods based on Mathematical Logic and Programming Language Semantics. Industrial experience, especially with embedded safety-critical software, would be an advantage. See https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:239002/type:job/where:4/apply:1 for the full announcement with more information and instructions on how to apply. The application deadline is December 31, 2018. Informal enquiries are welcome and may be sent to dil...@kth.se . Dilian Gurov, Associate Professor School of Electrical Engineering and Computer Science KTH Royal Institute of Technology https://www.csc.kth.se/~dilian/
[TYPES/announce] CSL 2017 Call for Participation
(University of Bruxelles), • Thomas Schwentick (TU Dortmund University), • Viorica Sofronie-Stokkermans (University of Koblenz-Landau), • Thomas Streicher (University of Darmstadt), • Jean-Marc Talbot (University of Aix-Marseille), • Luca Viganò (King's College London), • Ron van der Meyden (UNSW Australia), • Lijun Zhang (Chinese Academy of Sciences, Beijing). ORGANISING COMMITTEE • Stefan Buijsman, Department of Philosophy, Stockholm University • Mads Dam (OC co-chair), Department of Computer Science, KTH • Jacopo Emmenegger, Department of Mathematics, Stockholm University • Valentin Goranko (OC co-chair), Department of Philosophy, Stockholm University • Dilian Gurov (workshops chair), Department of Computer Science, KTH • Eric Johannesson, Department of Philosophy, Stockholm University • Vera Koponen, Department of Mathematics, Uppsala University • Johan Lindberg, Department of Mathematics, Stockholm University • Roussanka Loukanova, Department of Mathematics, Stockholm University • Peter LeFanu Lumsdaine, Department of Mathematics, Stockholm University • Anders Lundstedt, Department of Philosophy, Stockholm University • Karl Nygren, Department of Philosophy, Stockholm University • Erik Palmgren (OC co-chair), Department of Mathematics, Stockholm University CONTACTS AND ENQUIRIES -- With enquiries on organising matters, send email to: CSL2017philosophy.su.se With enquiries on scientific and programme issues, send email to: CSL2017easychair.org
[TYPES/announce] Logic Colloquium 2017: Call for Registration and Participation
) CONTRIBUTED TALKS: The call for submissions is already closed. There will be about 140 contributed talks, given in 6 parallel sessions. SOCIAL PROGRAMME: --- The social programme of LC 2017 will include a reception at Stockholm City Hall on August 14, a boat trip excursion on August 16, and a conference dinner on August 17. REGISTRATION -- The early registration fee, for students and participants from developing countries, is 1400 SEK including VAT (approx. 140 Euros) per participant, and includes coffee breaks and conference materials. For all others, the early registration fee is 2000 SEK including VAT. Late registration is 2800 SEK for regular fee participants, and 2000 SEK for reduced fee participants. Note: 500 SEK fee deduction when registering for CSL2017 at the same time. The registration fee does not cover accommodation, but there will be special offers at hostels and hotels (in the range 700 -1200 SEK per night for single rooms) available. Link for the registration page: https://www.math-stockholm.se/en/konferenser-och-akti/logic-in-stockholm-2/logic-in-stockholm-2017-august-7-25-1.718739 IMPORTANT DATES Main event: August 14-19, 2017 Joint session with CSL2017: August 20, 2017 Early registration deadline: June 9, 2017 Late registration deadline: August 1, 2017 PROGRAMME COMMITTEE --- - Rod Downey (University of Wellington) - Mirna Dzamonja (PC chair, University of East Anglia) - Ali Enayat (University of Gothenburg) - Fernando Ferreira (University of Lisbon) - Valentin Goranko (Stockholm University) - Martin Hils (University of Münster) - Sara Negri (University of Helsinki) - Assaf Rinot (Bar-Ilan University) - Igor Walukiewicz (University of Bordeaux) LOCAL ORGANISING COMMITTEE - Stefan Buijsman, Department of Philosophy, Stockholm University - Mads Dam, Department of Theoretical Computer Science, KTH - Jacopo Emmenegger, Department of Mathematics, Stockholm University - Valentin Goranko (OC co-chair), Department of Philosophy, Stockholm University - Dilian Gurov, Department of Theoretical Computer Science, KTH - Sven-Ove Hansson, Department of Philosophy, KTH Royal Institute of Technology - Eric Johannesson, Department of Philosophy, Stockholm University - Vera Koponen, Department of Mathematics, Uppsala University - Johan Lindberg, Department of Mathematics, Stockholm University - Roussanka Loukanova, Department of Mathematics, Stockholm University - Peter LeFanu Lumsdaine, Department of Mathematics, Stockholm University - Anders Lundstedt, Department of Philosophy, Stockholm University - Karl Nygren, Department of Philosophy, Stockholm University - Peter Pagin, Department of Philosophy, Stockholm University - Erik Palmgren (OC co-chair), Department of Mathematics, Stockholm University - Dag Westerståhl, Department of Philosophy, Stockholm University CONTACTS AND ENQUIRIES For enquiries on scientific and programme issues, send email to: Mirna Dzamonja (m.dzamo...@uea.ac.uk) For enquiries on organising matters, send email to: lc2017 at philosophy.su.se SPONSORS - Association for Symbolic Logic Stockholm University The GS Magnusson Foundation Prover Technology Stockholm City Hall
[TYPES/announce] CSL 2017: Call For Oral Presentations
aj Bjorner (Microsoft Research), • Maria Paola Bonacina (Università degli Studi di Verona), • Patricia Bouyer-Decitre (LSV, ENS Cachan), • Agata Ciabattoni (University of Viena), • Thierry Coquand (University of Gothenburg), • Mads Dam (KTH, Stockholm), PC co-chair • Ugo Dal Lago (University of Bologna), • Anuj Dawar (Cambridge University), • Valentin Goranko (Stockholm University), PC co-chair • Maribel Fernandez (King's College London), • Martin Grohe (RWTH Aachen), • Lauri Hella (University of Tampere), • Joost-Pieter Katoen (RWTH Aachen), • Orna Kupferman (University of Jerusalem), • Leonid Libkin (University of Edinburgh), • Angelo Montanari (University of Udine), • Catuscia Palamidessi (Paris, INRIA), • Frank Pfenning (Carnegie Mellon University, Pittsburgh) • Ram Ramanujam (Institute of Mathematical Sciences, Chennai), • Jean-Francois Raskin (University of Bruxelles), • Thomas Schwentick (TU Dortmund University), • Viorica Sofronie-Stokkermans (University of Koblenz-Landau), • Thomas Streicher (University of Darmstadt), • Jean-Marc Talbot (University of Aix-Marseille), • Luca Viganò (King's College London), • Ron van der Meyden (UNSW Australia), • Lijun Zhang (Chinese Academy of Sciences, Beijing). ORGANISING COMMITTEE • Mads Dam (OC co-chair), Department of Theoretical Computer Science, KTH • Valentin Goranko (OC co-chair), Department of Philosophy, Stockholm University • Dilian Gurov (Workshops chair), Department of Theoretical Computer Science, KTH • Roussanka Loukanova, Department of Mathematics, Stockholm University • Peter LeFanu Lumsdaine, Department of Mathematics, Stockholm University • Anders Lundstedt, Department of Philosophy, Stockholm University • Erik Palmgren (OC co-chair), Department of Mathematics, Stockholm University • Henning Strandin, Department of Philosophy, Stockholm University CONTACTS AND ENQUIRIES -- With enquiries on organising matters, send email to: CSL 2017philosophy.su.se With enquiries on scientific and programme issues, send email to: CSL 2017easychair.org
[TYPES/announce] CSL 2017: Final Call For Papers
page for the conference: https://easychair.org/conferences/?conf=CSL 2017. Submitted papers must be in English and must provide sufficient detail to allow the Programme Committee to assess the merits of the paper. Full proofs may appear in a clearly marked technical appendix which will be read at the reviewers' discretion. Authors are strongly encouraged to include a well written introduction which is directed at all members of the PC. Papers may not be submitted concurrently to another conference with refereed proceedings. The PC chairs should be informed of closely related work submitted to a conference or a journal. Papers authored or co-authored by members of the PC are not allowed. In addition, there will be an opportunity for short oral presentations at the conference. Abstracts for such oral presentations must be submitted through the Easychair submission webpage, under the category ``short presentations'', by June 4, 2017. They will not be included in the proceedings. PROGRAMME COMMITTEE --- • Parosh Aziz Abdulla (University of Uppsala), • Lars Birkedal (University of Aarhus), • Nikolaj Bjorner (Microsoft Research), • Maria Paola Bonacina (Università degli Studi di Verona), • Patricia Bouyer-Decitre (LSV, ENS Cachan), • Agata Ciabattoni (University of Viena), • Thierry Coquand (University of Gothenburg), • Mads Dam (KTH, Stockholm), PC co-chair • Ugo Dal Lago (University of Bologna), • Anuj Dawar (Cambridge University), • Valentin Goranko (Stockholm University), PC co-chair • Maribel Fernandez (King's College London), • Martin Grohe (RWTH Aachen), • Lauri Hella (University of Tampere), • Joost-Pieter Katoen (RWTH Aachen), • Orna Kupferman (University of Jerusalem), • Leonid Libkin (University of Edinburgh), • Angelo Montanari (University of Udine), • Catuscia Palamidessi (Paris, INRIA), • Frank Pfenning (Carnegie Mellon University, Pittsburgh) • Ram Ramanujam (Institute of Mathematical Sciences, Chennai), • Jean-Francois Raskin (University of Bruxelles), • Thomas Schwentick (TU Dortmund University), • Viorica Sofronie-Stokkermans (University of Koblenz-Landau), • Thomas Streicher (University of Darmstadt), • Jean-Marc Talbot (University of Aix-Marseille), • Luca Viganò (King's College London), • Ron van der Meyden (UNSW Australia), • Lijun Zhang (Chinese Academy of Sciences, Beijing). ORGANISING COMMITTEE • Mads Dam (OC co-chair), Department of Theoretical Computer Science, KTH • Valentin Goranko (OC co-chair), Department of Philosophy, Stockholm University • Dilian Gurov (Workshops chair), Department of Theoretical Computer Science, KTH • Roussanka Loukanova, Department of Mathematics, Stockholm University • Peter LeFanu Lumsdaine, Department of Mathematics, Stockholm University • Anders Lundstedt, Department of Philosophy, Stockholm University • Erik Palmgren (OC co-chair), Department of Mathematics, Stockholm University • Henning Strandin, Department of Philosophy, Stockholm University CONTACTS AND ENQUIRIES -- With enquiries on organising matters, send email to: CSL 2017philosophy.su.se With enquiries on scientific and programme issues, send email to: CSL 2017easychair.org
[TYPES/announce] CSL 2017: Second Call For Papers
the EasyChair page for the conference: https://easychair.org/conferences/?conf=CSL 2017. Submitted papers must be in English and must provide sufficient detail to allow the Programme Committee to assess the merits of the paper. Full proofs may appear in a clearly marked technical appendix which will be read at the reviewers' discretion. Authors are strongly encouraged to include a well written introduction which is directed at all members of the PC. Papers may not be submitted concurrently to another conference with refereed proceedings. The PC chairs should be informed of closely related work submitted to a conference or a journal. Papers authored or co-authored by members of the PC are not allowed. In addition, there will be an opportunity for short oral presentations at the conference. Abstracts for such oral presentations must be submitted through the Easychair submission webpage, under the category ``short presentations'', by June 4, 2017. They will not be included in the proceedings. PROGRAMME COMMITTEE --- • Parosh Aziz Abdulla (University of Uppsala), • Lars Birkedal (University of Aarhus), • Nikolaj Bjorner (Microsoft Research), • Maria Paola Bonacina (Università degli Studi di Verona), • Patricia Bouyer-Decitre (LSV, ENS Cachan), • Agata Ciabattoni (University of Viena), • Thierry Coquand (University of Gothenburg), • Mads Dam (KTH, Stockholm), PC co-chair • Ugo Dal Lago (University of Bologna), • Anuj Dawar (Cambridge University), • Valentin Goranko (Stockholm University), PC co-chair • Maribel Fernandez (King's College London), • Martin Grohe (RWTH Aachen), • Lauri Hella (University of Tampere), • Joost-Pieter Katoen (RWTH Aachen), • Orna Kupferman (University of Jerusalem), • Leonid Libkin (University of Edinburgh), • Angelo Montanari (University of Udine), • Catuscia Palamidessi (Paris, INRIA), • Frank Pfenning (Carnegie Mellon University, Pittsburgh) • Ram Ramanujam (Institute of Mathematical Sciences, Chennai), • Jean-Francois Raskin (University of Bruxelles), • Thomas Schwentick (TU Dortmund University), • Viorica Sofronie-Stokkermans (University of Koblenz-Landau), • Thomas Streicher (University of Darmstadt), • Jean-Marc Talbot (University of Aix-Marseille), • Luca Viganò (King's College London), • Ron van der Meyden (UNSW Australia), • Lijun Zhang (Chinese Academy of Sciences, Beijing). ORGANISING COMMITTEE • Mads Dam (OC co-chair), Department of Theoretical Computer Science, KTH • Valentin Goranko (OC co-chair), Department of Philosophy, Stockholm University • Dilian Gurov (Workshops chair), Department of Theoretical Computer Science, KTH • Roussanka Loukanova, Department of Mathematics, Stockholm University • Peter LeFanu Lumsdaine, Department of Mathematics, Stockholm University • Anders Lundstedt, Department of Philosophy, Stockholm University • Erik Palmgren (OC co-chair), Department of Mathematics, Stockholm University • Henning Strandin, Department of Philosophy, Stockholm University CONTACTS AND ENQUIRIES -- With enquiries on organising matters, send email to: CSL 2017philosophy.su.se With enquiries on scientific and programme issues, send email to: CSL 2017pcgmail.com
[TYPES/announce] CSL 2017: First Call For Papers
=CSL2017. Submitted papers must be in English and must provide sufficient detail to allow the Programme Committee to assess the merits of the paper. Full proofs may appear in a clearly marked technical appendix, which will be read at the reviewers' discretion. Authors are strongly encouraged to include a well written introduction which is directed at all members of the PC. Papers may not be submitted concurrently to another conference with refereed proceedings. The PC chairs should be informed of closely related work submitted to a conference or a journal. Papers authored or co-authored by members of the PC are not allowed. In addition, there will be an opportunity for short oral presentations at the conference. Abstracts for such oral presentations must be submitted through the Easychair submission webpage, under the category "short presentations", by June 4, 2017. They will not be included in the proceedings. PROGRAMME COMMITTEE --- • Parosh Aziz Abdulla (University of Uppsala), • Lars Birkedal (University of Aarhus), • Nikolaj Bjorner (Microsoft Research), • Maria Paola Bonacina (Università degli Studi di Verona), • Patricia Bouyer-Decitre (LSV, ENS Cachan), • Agata Ciabattoni (University of Viena), • Thierry Coquand (University of Gothenburg), • Mads Dam (KTH, Stockholm), PC co-chair • Ugo Dal Lago (University of Bologna), • Anuj Dawar (Cambridge University), • Valentin Goranko (Stockholm University), PC co-chair • Maribel Fernandez (King's College London), • Martin Grohe (RWTH Aachen), • Lauri Hella (University of Tampere), • Joost-Pieter Katoen (RWTH Aachen), • Orna Kupferman (University of Jerusalem), • Leonid Libkin (University of Edinburgh), • Angelo Montanari (University of Udine), • Catuscia Palamidessi (Paris, INRIA), • Frank Pfenning (Carnegie Mellon University, Pittsburgh), • Ram Ramanujam (Institute of Mathematical Sciences, Chennai), • Jean-Francois Raskin (University of Bruxelles), • Thomas Schwentick (TU Dortmund University), • Viorica Sofronie-Stokkermans (University of Koblenz-Landau), • Thomas Streicher (University of Darmstadt), • Jean-Marc Talbot (University of Aix-Marseille), • Luca Viganò (King's College London), • Ron van der Meyden (UNSW Australia), • Lijun Zhang (Chinese Academy of Sciences, Beijing). ORGANISING COMMITTEE • Mads Dam (OC co-chair), Department of Computer Science, KTH • Valentin Goranko (OC co-chair), Department of Philosophy, Stockholm University • Dilian Gurov (Workshops chair), Department of Computer Science, KTH • Roussanka Loukanova, Department of Mathematics, Stockholm University • Peter LeFanu Lumsdaine, Department of Mathematics, Stockholm University • Erik Palmgren (OC co-chair), Department of Mathematics, Stockholm University CONTACTS AND ENQUIRIES -- With enquiries on organising matters, send email to: CSL2017philosophy.su.se With enquiries on scientific and programme issues, send email to: CSL2017pcgmail.com =