Chers collègues,
La prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) aura lieu le
Mercredi 30 mai 2018 (11h--12h), Amphi IP11.
Vous trouverez sur le site du séminaire [1] les prochaines séances,
les résumés, captations vidéos et planches des exposés précédents [2],
le détail de cette séance [3] ainsi que le plan d'accès [4].
[1]
http://seminaire.lrde.epita.fr
[2]
http://seminaire.lrde.epita.fr/Archives
[3]
http://seminaire.lrde.epita.fr/2018-05-30
[4]
http://www.lrde.epita.fr/wiki/Contact
Au programme du Mercredi 30 mai 2018 :
* 11h--12h: Partial but Precise Loop Summarization and Its Applications
-- Jan Strejcek, Masaryk University
https://www.fi.muni.cz/~xstrejc/
We show a symbolic-execution-based algorithm computing the precise
effect of a program cycle on program variables. For a program
variable,
the algorithm produces an expression representing the variable value
after the number of cycle iterations specified by parameters of the
expression. The algorithm is partial in the sense that it can fail to
find such an expression for some program variables (for example, it
fails in cases where the variable value depends on the order of paths
in
the cycle taken during iterations).
We present two applications of this loop summarization procedure. The
first is the construction of a nontrivial necessary condition on
program
input to reach a given program location. The second application is a
loop bound detection algorithm, which produces tighter loop bounds
than
other approaches.
-- Jan Strejcek is an associate professor at the Faculty of
Informatics of Masaryk University located in Brno, Czech Republic. He
received his PhD in Computer Science (2005) and Master degrees in
Mathematics (2000) and Computer Science (2001) from the same
university.
His current research focuses on automata over infinite words,
automatic
program analysis, and SMT-solving of quantified bitvector formulae.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible. N'hésitez pas à nous faire
parvenir vos suggestions d'orateurs.
--
Guillaume TOCHON
Maître de conférences // Assistant Professor
LRDE, EPITA
18, rue Pasteur
94270 Le Kremlin-Bicêtre