[TYPES/announce] PhD Position in Deductive Verification of Safety-Critical Software

2021-11-17 Thread Dilian Gurov

[ 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

2019-04-25 Thread Dilian Gurov

[ 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

2018-12-10 Thread Dilian Gurov

[ 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

2017-06-30 Thread Dilian Gurov
 (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

2017-06-03 Thread Dilian Gurov
)



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

2017-05-18 Thread Dilian Gurov
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

2017-03-03 Thread Dilian Gurov
 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

2017-01-19 Thread Dilian Gurov
 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

2016-11-11 Thread Dilian Gurov
=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


=