This page gathers information on internship opportunities at LSV.

Some internships are paid; this topic should be discussed with the supervisors.

LSV welcomes postdoctoral researchers willing to broaden their PhD work in one of our research themes.

LSV seeks students about to start a PhD in one of our research themes.

The subjects presented below range from the practical aspects of verification to rather fundamental issues. Funding might depend on the exact subject or on other specific requirements. Prospective students should contact theses@lsv.ens-cachan.fr, attach their curriculum vitae, and explain which subject(s) they are interested in.

PhD studies lead to public and private research employment, teaching positions in universities, etc. Here is for information what became of the LSV graduates.

The following internships are intended for students in their second year of MSc studies.

- Observe locally, control globally (S. Haar, S. Schwoon)
- Developping a standard library for Lambdapi (F. Blanqui)
- Automated reasoning in a meta-logic for cryptographic protocols (D. Baelde, A. Koutsos)
- Verification of security protocols - Squirrel prover (D. Baelde, S. Delaune)
- Structured proofs in Dedukti (F. Blanqui)
- Specification and Verification of Properties of Neural Networks (S. Haddad)
- Importing Logipedia proofs in Agda (F. Blanqui)
- Updates in Description Logics (S. Demri)
- Formalisation d'un langage graphique à bloc pour la preuve de programme (G. Dowek)
- WQO Finitary Powersets: Complexity and Algorithms (S. Schmitz, Ph. Schnoebelen)
- Deciding the Logic of Subsequences (Ph. Schnoebelen)
- Algorithms for Expected-Time Reachability (L. Doyen)
- Graph and Automata Algorithms for Verification (L. Doyen)
- Model Checking Well Structured Transition Systems (A. Finkel)
- Well Structured FIFO Automata (A. Finkel)

The following internships are intended for students in their first year of MSc studies.

- Test for Posix Utilities (M. Sighireanu, R. Treinen)
- Solver for Feature Tree Logic (M. Sighireanu, R. Treinen)
- Observe locally, control globally (S. Haar, S. Schwoon)
- Developping a standard library for Lambdapi (F. Blanqui)
- Structured proofs in Dedukti (F. Blanqui)
- Specification and Verification of Properties of Neural Networks (S. Haddad)
- Importing Logipedia proofs in Agda (F. Blanqui)
- Modern user interface for interactive theorem proving (F. Blanqui)
- Model Checking Well Structured Transition Systems (A. Finkel)
- Well Structured FIFO Automata (A. Finkel)

The following internships are mostly (but not exclusively) intended for students in their first year of studies at *École Normale Supérieure de Lyon* or *École Normale Supérieure de Paris*.

- Test for Posix Utilities (M. Sighireanu, R. Treinen)
- Solver for Feature Tree Logic (M. Sighireanu, R. Treinen)
- Developping a standard library for Lambdapi (F. Blanqui)
- Structured proofs in Dedukti (F. Blanqui)
- Importing Logipedia proofs in Agda (F. Blanqui)
- Modern user interface for interactive theorem proving (F. Blanqui)