Difference between revisions of "Phd and internship subjects"

From Numerical Transition Systems
Jump to: navigation, search
 
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]

Latest revision as of 20:27, 8 December 2024

Internship subjects

The goal of this internship is an implementation of a toolbox that handles sets of graphs described as regular grammars. Ideally, such a toolbox should support the boolean operations of union, intersection and complement and decide the problems of membership and inclusion, by building finite recognizer algebras from the syntactic description of sets, as regular grammars.

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.

Retrieved from "http://nts.imag.fr/index.php?title=Phd_and_internship_subjects&oldid=1209"