Difference between revisions of "Phd and internship subjects"
Radu iosif (Talk | contribs) |
Radu iosif (Talk | contribs) |
||
| (6 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | |||
== PhD subjects == | == PhD subjects == | ||
| − | |||
| − | * [ | + | * [https://nts.imag.fr/images/6/6f/Phd-pavedys.pdf Formal Modeling and Verification of Parameterized and Distributed Systems] |
| − | + | Applications of distributed systems are omnipresent, allowing to share resources and coordinate activities between geographically distributed parties. Designing, understanding, and validating distributed systems is challenging because of the huge number of interactions between components, some potentially leading to unpredictable scenarios. Mechanizing the analysis and verification of distributed systems is notoriusly difficult. Recently, there has been a notable trend to apply interactive theorem provers, i.e., using proof assistants, to the task. We propose to develop a complementary set of verification methods based, on generalizations of the more mechanized methods from the model-checking and automated theorem proving communities | |
| − | |||
| − | |||
| − | |||
== Internship subjects == | == Internship subjects == | ||
| + | * [https://nts.imag.fr/images/8/8a/MSOBTW.pdf A Solver for Monadic Second Order Logic of Graphs of Bounded Tree-width] | ||
| − | + | The goal of this internship is to first try the direct implementation | |
| − | + | that follows Courcelle's proof, identity its bottlenecks and, second, | |
| − | The goal of this internship is the | + | devises solutions by generating more compact MSO formulae over |
| + | trees, that postpone (or even avoid) state explosion, in some cases. | ||
* [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. | ||
| − | |||
| − | |||
| − | |||
| − | |||
Latest revision as of 10:11, 29 May 2024
PhD subjects
Applications of distributed systems are omnipresent, allowing to share resources and coordinate activities between geographically distributed parties. Designing, understanding, and validating distributed systems is challenging because of the huge number of interactions between components, some potentially leading to unpredictable scenarios. Mechanizing the analysis and verification of distributed systems is notoriusly difficult. Recently, there has been a notable trend to apply interactive theorem provers, i.e., using proof assistants, to the task. We propose to develop a complementary set of verification methods based, on generalizations of the more mechanized methods from the model-checking and automated theorem proving communities
Internship subjects
The goal of this internship is to first try the direct implementation that follows Courcelle's proof, identity its bottlenecks and, second, devises solutions by generating more compact MSO formulae over trees, that postpone (or even avoid) state explosion, in some cases.
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.
