Difference between revisions of "Phd and internship subjects"
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
| Line 1: | Line 1: | ||
| − | |||
== PhD subjects == | == PhD subjects == | ||
| − | |||
* [http://nts.imag.fr/images/d/d7/SelfAdaptingLogicsPhd.pdf Logical Foundations of Self-Adapting Distributed Systems] | * [http://nts.imag.fr/images/d/d7/SelfAdaptingLogicsPhd.pdf Logical Foundations of Self-Adapting Distributed Systems] | ||
Reconfiguration is an inherent aspect of modern distributed systems, such as clouds or IoT. Processes can be created or removed due to internal faults, redistribution of resources, workload or traffic changes. Moreover, the shape of the communication network may change. Self-adapting systems initiate and carry out reconfiguration sequences automatically, in order to avoid expensive or even mission-critical downtimes, required by manual reconfiguration. The successful candidate will develop logics and automated reasoning techniques that enable writing formal proofs of correctness of self-adapting distributed systems. We focus on logics that describe the shape of a network (i.e., the interconnection of processes via communication channels) and how this shape changes with time. Particular attention will be devoted to the implementation of practical verification tools based on automated theorem proving and model checking based on the logics developped in this thesis. To this end, the candidate is expected to work on implementation and prototyping, in addition to theoretical research. | Reconfiguration is an inherent aspect of modern distributed systems, such as clouds or IoT. Processes can be created or removed due to internal faults, redistribution of resources, workload or traffic changes. Moreover, the shape of the communication network may change. Self-adapting systems initiate and carry out reconfiguration sequences automatically, in order to avoid expensive or even mission-critical downtimes, required by manual reconfiguration. The successful candidate will develop logics and automated reasoning techniques that enable writing formal proofs of correctness of self-adapting distributed systems. We focus on logics that describe the shape of a network (i.e., the interconnection of processes via communication channels) and how this shape changes with time. Particular attention will be devoted to the implementation of practical verification tools based on automated theorem proving and model checking based on the logics developped in this thesis. To this end, the candidate is expected to work on implementation and prototyping, in addition to theoretical research. | ||
| − | |||
== Internship subjects == | == Internship subjects == | ||
| − | |||
* [http://nts.imag.fr/images/5/5e/InfiniteAlphabetAutomata.pdf Verifying Concurrent Systems with Automata over Infinite Alphabets] | * [http://nts.imag.fr/images/5/5e/InfiniteAlphabetAutomata.pdf Verifying Concurrent Systems with Automata over Infinite Alphabets] | ||
The goal of this internship is to study extensions of finite-state automata over infinite alphabets and apply them to the verification of concurrent and distributed systems with unbounded numbers of threads. The internship comprises theoretical as well as implementation work, and will explore orthogonal domains, such as logic, automata theory and concurrency. | The goal of this internship is to study extensions of finite-state automata over infinite alphabets and apply them to the verification of concurrent and distributed systems with unbounded numbers of threads. The internship comprises theoretical as well as implementation work, and will explore orthogonal domains, such as logic, automata theory and concurrency. | ||
Revision as of 15:28, 2 June 2023
PhD subjects
Reconfiguration is an inherent aspect of modern distributed systems, such as clouds or IoT. Processes can be created or removed due to internal faults, redistribution of resources, workload or traffic changes. Moreover, the shape of the communication network may change. Self-adapting systems initiate and carry out reconfiguration sequences automatically, in order to avoid expensive or even mission-critical downtimes, required by manual reconfiguration. The successful candidate will develop logics and automated reasoning techniques that enable writing formal proofs of correctness of self-adapting distributed systems. We focus on logics that describe the shape of a network (i.e., the interconnection of processes via communication channels) and how this shape changes with time. Particular attention will be devoted to the implementation of practical verification tools based on automated theorem proving and model checking based on the logics developped in this thesis. To this end, the candidate is expected to work on implementation and prototyping, in addition to theoretical research.
Internship subjects
The goal of this internship is to study extensions of finite-state automata over infinite alphabets and apply them to the verification of concurrent and distributed systems with unbounded numbers of threads. The internship comprises theoretical as well as implementation work, and will explore orthogonal domains, such as logic, automata theory and concurrency.
