Difference between revisions of "Internship subjects"

From Numerical Transition Systems
Jump to: navigation, search
(One intermediate revision by the same user not shown)
Line 1: Line 1:
 
The following internships can be continued by a PhD thesis:  
 
The following internships can be continued by a PhD thesis:  
  
* [http://nts.imag.fr/images/8/85/ArchitectureSeparationLogic.pdf Local Reasoning about Reconfigurable Component-based Systems] (Master level, 6 months)
+
* [http://nts.imag.fr/images/8/85/ArchitectureSeparationLogic.pdf Local Reasoning about Reconfigurable Component-based Systems]  
  
 
The goal of this internship is the study of logics for the design and verification of complex component-based distributed applications, using the principles of locality (the ability to describe the effect of an update only from the parts involved while gnoring the ones unchanged) and compositionality (the ability to join the results of local analyses into a global condition capturing the correctness requirement for the entire system). During this internship, the candidate will aquire command of advanced theoretical notions of logics and system verification. The internship comprises theoretical as well as implementation work.  
 
The goal of this internship is the study of logics for the design and verification of complex component-based distributed applications, using the principles of locality (the ability to describe the effect of an update only from the parts involved while gnoring the ones unchanged) and compositionality (the ability to join the results of local analyses into a global condition capturing the correctness requirement for the entire system). During this internship, the candidate will aquire command of advanced theoretical notions of logics and system verification. The internship comprises theoretical as well as implementation work.  
  
* [http://nts.imag.fr/images/5/5e/InfiniteAlphabetAutomata.pdf Verifying Concurrent Systems with Automata over Infinite Alphabets] (Master level, 6 months)
+
* [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.
  
* [Decision Procedures for Separation Logic Modulo Theories of Data] (Master level, 6 months)
+
* [http://nts.imag.fr/images/3/32/SeparationLogicEntailmentChecking.pdf Decision Procedures for Separation Logic Modulo Theories of Data]  
  
 
The goal of this internship is to study the combination of Separation Logic with data theories supported by SMT solvers. The internship comprises theoretical as well as implementation work.
 
The goal of this internship is to study the combination of Separation Logic with data theories supported by SMT solvers. The internship comprises theoretical as well as implementation work.

Revision as of 18:16, 23 January 2021

The following internships can be continued by a PhD thesis:

The goal of this internship is the study of logics for the design and verification of complex component-based distributed applications, using the principles of locality (the ability to describe the effect of an update only from the parts involved while gnoring the ones unchanged) and compositionality (the ability to join the results of local analyses into a global condition capturing the correctness requirement for the entire system). During this internship, the candidate will aquire command of advanced theoretical notions of logics and system verification. The internship comprises theoretical as well as implementation work.

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 the combination of Separation Logic with data theories supported by SMT solvers. The internship comprises theoretical as well as implementation work.