Phd and internship subjects - Revision history

Radu iosif at 19:27, 8 December 2024

2024-12-08T19:27:30Z

Radu iosif at 19:27, 8 December 2024

2024-12-08T19:27:05Z

Radu iosif at 18:00, 8 December 2024

2024-12-08T18:00:13Z

Radu iosif at 09:11, 29 May 2024

2024-05-29T09:11:38Z

Radu iosif at 16:44, 27 October 2023

2023-10-27T16:44:40Z

Radu iosif at 16:43, 27 October 2023

2023-10-27T16:43:52Z

Radu iosif at 14:28, 2 June 2023

2023-06-02T14:28:06Z

Radu iosif at 14:27, 2 June 2023

2023-06-02T14:27:23Z

Radu iosif at 11:14, 26 May 2023

2023-05-26T11:14:08Z

Radu iosif at 11:10, 26 May 2023

2023-05-26T11:10:54Z

← Older revision		Revision as of 19:27, 8 December 2024
Line 1:		Line 1:
−	== ~~PhD~~ subjects ==	+	== Internship 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 ==~~

	* [http://nts.imag.fr/images/b/b1/TW2REG.pdf A Toolbox for Handling Infinite Sets of Graphs]		* [http://nts.imag.fr/images/b/b1/TW2REG.pdf A Toolbox for Handling Infinite Sets of Graphs]

@@ Line 16: / Line 16: @@
 building finite recognizer algebras from the syntactic description of
 sets, as regular grammars.
 * [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.

@@ Line 8: / Line 8: @@
 == Internship subjects ==
-* [https://nts.imag.fr/images/8/8a/MSOBTW.pdf A Solver for Monadic Second Order Logic of Graphs of Bounded Tree-width]
+* [http://nts.imag.fr/images/b/b1/TW2REG.pdf A Toolbox for Handling Infinite Sets of Graphs]
 * [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.

@@ Line 1: / Line 1: @@
 == PhD subjects ==
-* [http://nts.imag.fr/images/d/d7/SelfAdaptingLogicsPhd.pdf Logical Foundations of Self-Adapting Distributed Systems]
+* [https://nts.imag.fr/images/6/6f/Phd-pavedys.pdf Formal Modeling and Verification of Parameterized and Distributed Systems]
 == Internship subjects ==

@@ Line 7: / Line 7: @@
 == Internship subjects ==
-* [A Solver for Monadic Second Order Logic of Graphs of Bounded Tree-width]
+* [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

← Older revision		Revision as of 11:10, 26 May 2023
Line 2:		Line 2:
	== PhD subjects ==		== 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.

−	* [http://nts.imag.fr/images/5/58/Reconfiguration.pdf Proving Correctness of Reconfigurable Systems]
−
−	The goal of this PhD project is the development of a rigourous design framework for distributed systems, that uses verification from the early stages of model building. Formal verification is the process of transforming a query about the correctness of a system (e.g. is every store request to a cloud treated by storing the data in such a way that any future retrieval request will eventually find it?) into a logical validity query (is a given formula true in general?) that can be handled by automated reasoning techniques (theorem proving). Hence, we recognise logic, automated reasoning and model checking as being the main ingredients of formal verification, and also central research topics in our project.
−
−	* [http://nts.imag.fr/images/2/25/SepLogDataPhD.pdf Decision Procedures for Inductive Separation Logic Modulo Data Theories]
−
−	The goal of this PhD project is to devise a decision procedure for Separation Logic with user-provided inductive definitions of predicates. We intend to find a procedure that is optimal from a theoretical point of view, practically efficient, and able to handle a class of definitions that is as large as possible, combining spatial reasoning (to reason on the shape of the considered data structures) with data theory reasoning based on external tools (to take into account the properties of the data stored inside the structure).

	== Internship subjects ==		== Internship subjects ==