BEGIN:VCALENDAR VERSION:2.0 PRODID:-//129.88.40.24//NONSGML kigkonsult.se iCalcreator 2.20.4// CALSCALE:GREGORIAN METHOD:PUBLISH X-WR-CALNAME:Software Verification Seminar X-WR-CALDESC:Software Verification Seminar X-WR-TIMEZONE:Europe/Paris BEGIN:VEVENT UID:20260705T081935UTC-6648GDerkn@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Thursday 27 April 2017 - Auditoriu m (IMAG) = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 13:30 - Salle : Auditorium (IMAG) George Karpenkov\, VERIMAG http://m etaworld.me « Finding Inductive Invariants using SMT Solving and Convex Opt imization » Abstract: Static analysis concerns itself with deriving program properties which hold\nuniversally for all program executions.\nSuch prop erties are used for proving program properties (e.g. there never\noccurs a n overflow or other runtime error regardless of a particular execution) an d are almost\ninvariably established using inductive invariants: propertie s which hold\nfor the initial state and imply themselves... DTSTART:20170427T133000 DTEND:20170427T153000 DURATION:PT2H0M0S LOCATION:Auditorium (IMAG) SUMMARY:George Karpenkov - Finding Inductive Invariants using SMT Solving a nd Convex Optimization END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-66509s8fUJ@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Wednesday 22 March 2017 - Rm. 204 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 13 :30 - Salle : Rm. 204 George Karpenkov\, VERIMAG http://metaworld.me « (PhD D efense Rehearsal): Finding Inductive Invariants using SMT Solving and Conv ex Optimization » Abstract: Static analysis concerns itself with deriving p rogram properties which hold\nuniversally for all program executions.\nSuc h properties are used for proving program properties (e.g. there never\noc curs an overflow or other runtime error regardless of a particular executi on) and are almost\ninvariably established using inductive invariants: pro perties which hold\nfor the initial state and imply... DTSTART:20170322T133000 DTEND:20170322T150000 DURATION:PT1H30M0S LOCATION:Rm. 204 SUMMARY:George Karpenkov - (PhD Defense Rehearsal): Finding Inductive Invar iants using SMT Solving and Convex Optimization END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6651nujivv@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 10 January 2017 - 206\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n 14:00 - Salle : 206\n\nCristina Serban\, VERIMAG\n\n\n« Reasoning in the B ernays-Schonfinkel-Ramsey Fragment of Separation Logic » \n\nAbstract:\n\n Separation Logic (SL) is a well-known assertion language used in Hoare-sty le modular proof systems for programs with dynamically allocated data stru ctures. In this paper we investigate the fragment of first-order SL restri ctedto the Bernays-Schonfinkel-Ramsey quantifier prefix ∃∗∀∗\, where the q uantified variables range over the set of memory locations. When this set is uninterpreted (has no associated theory) the fragment is... DTSTART:20170110T140000 DTEND:20170110T150000 DURATION:PT1H0M0S LOCATION:206 SUMMARY:Cristina Serban - Reasoning in the Bernays-Schonfinkel-Ramsey Fragm ent of Separation Logic END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-665267APVD@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Friday 4 November 2016 - Room 204 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 1 3:00 - Salle : Room 204 George Karpenkov\, VERIMAG http://metaworld.me « Form ula Slicing: Inductive Invariants from Preconditions » Abstract: We propose a ``formula slicing'' method for finding inductive invariants.\nIt is bas ed on the observation that many loops in the program\naffect only a small part of the memory\,\nand many invariants which were valid before a loop a re still valid after.\n\nGiven a precondition of the loop\,\nobtained from the preceding program fragment\,\nwe weaken it until it becomes inductive .\nThe weakening procedure is guided by... DTSTART:20161104T130000 DTEND:20161104T140000 DURATION:PT1H0M0S LOCATION:Room 204 SUMMARY:George Karpenkov - Formula Slicing: Inductive Invariants from Preco nditions END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6652Rf25Pg@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Friday 7 October 2016 - IMAG 206 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 14 :00 - Salle : IMAG 206 David Monniaux\, CNRS / VERIMAG http://www-verimag.im ag.fr/~monniaux/ « Cell morphing: from array programs to array-free Horn cl auses » Abstract: Automatically verifying safety properties of programs is hard. Many approaches exist for verifying\nprograms operating on Boolean a nd integer values (e.g. abstract interpretation\, counterexample-guided\na bstraction refinement using interpolants)\, but transposing them to array properties has been fraught with difficulties. Our work addresses that iss ue with a powerful and flexible abstraction\, parametric... DTSTART:20161007T140000 DTEND:20161007T150000 DURATION:PT1H0M0S LOCATION:IMAG 206 SUMMARY:David Monniaux - Cell morphing: from array programs to array-free H orn clauses END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6653PK2hWp@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Tuesday 14 June 2016 - IMAG 206 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 13:3 0 - Salle : IMAG 206 Julien Braine\, École normale supérieure de Lyon « Usin g abstract interpretation on Horn clauses: arrays and lists » Abstract: Aut omatically verifying safety properties of programs is a tough problem that has been tackled\nusing many different approaches: rewriting systems\, ab stract interpretation\, SMT solving.\nMost techniques restrict themselves to programs operating on Boolean and integer values and\ntransposing them to infinite data structures such as arrays has not yet been satisfyingly a chieved.\nRecent work by Monniaux and Gonnord suggests to... DTSTART:20160614T133000 DTEND:20160614T143000 DURATION:PT1H0M0S LOCATION:IMAG 206 SUMMARY:Julien Braine - Using abstract interpretation on Horn clauses: arra ys and lists END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6654mdU20O@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 7 June 2016 - IMAG 206 \n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n14:00 - Salle : IMAG 206\n\nCharlotte Truchet\, Université de Nantes\nh ttps://www.normalesup.org/~truchet/\n\n« constraints programming & abstrac t interpretation » \n\nAbstract:\n\nFirst an introduction to constraints p rogramming\, then relationship to abstract interpretation.\n\n\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nOther sem inars at VERIMAG - http://www-verimag.imag.fr/Verimag-Seminars\,62.html?la ng=en\nLocation/Vision: IMAG 206 - \nTo unsubscribe\, reply to this mail w ith UNSUBSCRIBE in the subject\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = =... DTSTART:20160607T140000 DTEND:20160607T150000 DURATION:PT1H0M0S LOCATION:IMAG 206 SUMMARY:Charlotte Truchet - constraints programming & abstract interpretati on END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6655jvaWo0@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Wednesday 23 March 2016 - salle A. Turing CE4 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 14:00 - Salle : salle A. Turing CE4 Radu Iosif\, Verimag http://nt s.imag.fr/index.php/Radu_Iosif « Selected TACAS 2016 Papers: a joint Softwa re Analysis and Tempo seminar » Abstract: Dogan Ulus: Online Timed Pattern Matching\n\nTimed pattern matching consists in finding all segments of a d ensetime\nBoolean signal that match a pattern defined by a timed regular e xpression.\nThis problem has been formulated and solved in [17] via an off line algorithm that takes the signal and expression as inputs and produces the set of all matches\, represented as a finite union of... DTSTART:20160323T140000 DTEND:20160323T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Radu Iosif - Selected TACAS 2016 Papers: a joint Software Analysis and Tempo seminar END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6655VauEZA@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Thursday 3 March 2016 - salle A. Turing CE4 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 15:00 - Salle : salle A. Turing CE4 George Karpenkov\, VERIMAG http ://metaworld.me « Introduction to SMT & JavaSMT: A Unified Library for Util izing SMT Solvers » Abstract: The talk is split in two short parts.\nThe fi rst part is by David Monniaux.\n\nDavid will give an introduction to satis fiability modulo theory:\n- what it is\n- how solvers are used\n- usual th eories\n- limitations\n\nThe second part is by George Karpenkov.\nGeorge w ill give a short talk on the newly developed JavaSMT tool (https://github. com/sosy-lab/java-smt/)\, which can be used for posing... DTSTART:20160303T150000 DTEND:20160304T070000 DURATION:PT16H0M0S LOCATION:salle A. Turing CE4 SUMMARY:George Karpenkov - Introduction to SMT & JavaSMT: A Unified Library for Utilizing SMT Solvers END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6656KLVU7b@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Monday 7 December 2015 - salle A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n14:00 - Salle : salle A. Turing CE4\n\nAnicet Bart\, École des Mines de Nantes / LINA\nhttp://anicet.bart.free.fr/\n\n« Verifying a Real-Time Language with Constraints » \n\nAbstract:\n\nFormal verification of real time programs\, where variables can be assigned different values at every single time\, is difficult due to the analyses of loops with time lags. In this talk\, we consider a problem arising from verification of r eal- time languages: checking of the range of stream variables. We present a constraint model for this problem\, and an algorithm\, combining constr aint... DTSTART:20151207T140000 DTEND:20151207T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Anicet Bart - Verifying a Real-Time Language with Constraints END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6657spOFFI@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Thursday 26 February 2015 - salle A. Turing CE4 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 14:00 - Salle : salle A. Turing CE4 George Karpenkov\, VERIMAG « Scalable Code Analysis with Policy Iteration » Abstract: We present a new algorithm for deriving numerical invariants\nwhich combines the precision of max-policy iteration with the flexibility\nand scalability of conventio nal Kleene iterations.\nIt is stated using Configurable Program Analysis\n framework\, thus allowing inter-analysis communication.\nWe augment the al gorithm with adjustable block encoding\, which gives better\nresults than the existing path focusing approach\, and with a novel... DTSTART:20150226T140000 DTEND:20150226T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:George Karpenkov - Scalable Code Analysis with Policy Iteration END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6657uTO7Ec@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Wednesday 17 December 2014 - sal le A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n14:00 - Salle : salle A. Turing CE4\n\nRadu IOSIF\, VER IMAG\nhttp://www-verimag.imag.fr/\n\n« Deciding Entailments in Inductive S eparation Logic with Tree Automata » \n\nAbstract:\n\nSeparation Logic (SL ) with inductive definitions is a natural formalism for specifying complex recursive data structures\, used in compositional verification of program s manipulating such structures. The key ingredient of any automated verifi cation procedure based on SL is the decidability of the entailment problem . In this work\, we reduce the entailment problem for a non-trivial subset of SL... DTSTART:20141217T140000 DTEND:20141217T160000 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Radu IOSIF - Deciding Entailments in Inductive Separation Logic wit h Tree Automata END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6658pvJIV5@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 14 October 2014 - salle A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n10:30 - Salle : salle A. Turing CE4\n\nAntoine Miné\, CNRS / ENS-Paris\nhttp://www.di.ens.fr/~mine/\n\n« tba » \n\nAbstract:\n\ntba \n\n\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nOther seminars at VERIMAG - http://www-verimag.imag.fr/Verimag-Semi nars\,62.html?lang=en\nLocation/Vision: salle A. Turing CE4 - http://www-v erimag.imag.fr/Plan-d-acces.html?lang=fr\nTo unsubscribe\, reply to this m ail with UNSUBSCRIBE in the subject\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = DTSTART:20141014T103000 DTEND:20141014T221500 DURATION:PT11H45M0S LOCATION:salle A. Turing CE4 SUMMARY:Antoine Miné - tba END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-66596EVz3g@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 9 September 2014 - sall e A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n14:30 - Salle : salle A. Turing CE4\n\nDorian Nogneng\, École polytechnique\n\n\n« fonctions de Schur » \n\nRésumé :\n\nExposé du stage de Dorian Nogneng à University of Western Ontario.\n\n\n\n\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nOther s eminars at VERIMAG - http://www-verimag.imag.fr/Verimag-Seminars\,62.html? lang=en\nLocation/Vision: salle A. Turing CE4 - http://www-verimag.imag.fr /Plan-d-acces.html?lang=fr\nTo unsubscribe\, reply to this mail with UNSUB SCRIBE in the subject\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =... DTSTART:20140909T143000 DTEND:20140909T153000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Dorian Nogneng - fonctions de Schur END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6659UIUkII@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Friday 6 June 2014 - salle A. Tur ing CE4 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 14:00 - Salle : salle A. Turing CE4 Philipp Wendler\, Universität Pas sau http://www.philippwendler.de/ « Combining k-Induction with Continuously- Refined Invariants » Abstract: Bounded model checking (BMC) is a well-known and successful technique for finding bugs in software.\n\nk-induction is an approach to extend BMC-based approaches from falsification to verificat ion.\n\nAutomatically generated auxiliary invariants can be used to streng then\nthe induction hypothesis. We improve this approach and further incre ase effectiveness and\nefficiency in the following way:... DTSTART:20140606T140000 DTEND:20140606T150000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Philipp Wendler - Combining k-Induction with Continuously-Refined I nvariants END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6660EjHMgh@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Monday 2 June 2014 - salle A. Tur ing CE4 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 15:30 - Salle : salle A. Turing CE4 Gustavo Grieco\, Université de Ro sario (Argentina) et Verimag « On some ideas for vulnerability discovery us ing Machine Learning » Abstract: A typical OS usually involves thousands of executable files.\nFor these programs\, we can have thousands of bugs rep orts. \nFuzzing and detecting vulnerabilities at the OS scale leads to\nne w issues and challenges. We think can address these using\na combination o f dynamic/static program analysis with Machine Learning\ntechniques in ord er to learn pattern to discover vulnerable programs\nand... DTSTART:20140602T153000 DTEND:20140602T163000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Gustavo Grieco - On some ideas for vulnerability discovery using Ma chine Learning END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-66619LtIrH@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Tuesday 13 May 2014 - salle A. Tur ing CE4 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 15:30 - Salle : salle A. Turing CE4 Sudakshina Das\, Oxford Universit y « Significance of Liveness based approach to Pointer Analysis » Abstract: A flow and context sensitive pointer analysis is known to be very precise but is also\ninfamous to be highly inefficient. Almost all approaches to p ointer analysis are done with\napproximations that is with either flow or context sensitivity but seldom with both. In fact\nGCC’s pointer analysis pass ′ pta ′ is done with neither. But what if we look at this with a\ncom pletely new perpective? The fundamental problem... DTSTART:20140513T153000 DTEND:20140513T163000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Sudakshina Das - Significance of Liveness based approach to Pointer Analysis END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-66624Uodbd@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Monday 14 April 2014 - salle A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n15:00 - Salle : salle A. Turing CE4\n\nCesare Tinelli\, Unive rsity of Iowa\nhttp://homepage.cs.uiowa.edu/~tinelli/\n\n« Incremental Inv ariant Generation using Logic-based Automatic Abstract Transformers » \n\n Abstract:\n\nFormal analysis tools for system models often require or bene fit from the availability of auxiliary system invariants. Abstract interpr etation is currently one of the best approaches for discovering useful inv ariants\, in particular numerical ones. However\, its application is limit ed by two orthogonal issues: (i) developing an abstract interpretation is often... DTSTART:20140414T150000 DTEND:20140414T160000 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Cesare Tinelli - Incremental Invariant Generation using Logic-based Automatic Abstract Transformers END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-66633KBiwg@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Monday 31 March 2014 - salle A. Pn ueli CE3 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 14:30 - Salle : salle A. Pnueli CE3 Francesco Alberti\, University o f Lugano and VERIMAG http://www.inf.usi.ch/phd/alberti/ « Decision Procedure s for Flat Array Properties » Abstract: We present new decidability results for quantified fragments of theories of arrays.\nOur decision procedures are fully declarative\, parametric in the theories of indexes and elements and orthogonal with respect to known results.\nWe also discuss applicatio ns to the analysis of programs handling arrays.\nThis is a joint work with S. Ghilardi and N. Sharygina = = = = = = = = = = = = =... DTSTART:20140331T143000 DTEND:20140331T153000 DURATION:PT1H0M0S LOCATION:salle A. Pnueli CE3 SUMMARY:Francesco Alberti - Decision Procedures for Flat Array Properties END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-66635U9puR@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 25 March 2014 - salle A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n15:45 - Salle : salle A. Turing CE4\n\nLaurent Mounier\, VER IMAG\nhttp://www-verimag.imag.fr/~mounier\n\n« Lazart : une approche symbo lique pour évaluer la robustesse d'un code aux attaques par injection de f autes (Lazart: a symbolic approach for evaluating the robustness of secure d codes against control flow fault injections ) » \n\nRésumé :\n\nDans le domaine des cartes à puces\, il est nécessaire de protéger les equipement s contre toutes attaques potentiellement dangereuses pour leur sécurité. L es normes de développement de type Critères Communs exigent d'effectuer... DTSTART:20140325T154500 DTEND:20140325T164500 DURATION:PT1H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Laurent Mounier - Lazart : une approche symbolique pour évaluer la robustesse d'un code aux attaques par injection de fautes (Lazart: a symbo lic approach for evaluating the robustness of secured codes against contr ol flow fault injections ) END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6664JnzJXk@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 18 March 2014 - salle A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n15:45 - Salle : salle A. Turing CE4\n\nRadu Iosif\, Verimag \n\n\n« The Tree Width of Separation Logic with Recursive Definitions » \n \nAbstract:\n\nSeparation Logic is a widely used formalism for describing dynamically allocated linked data structures\, such as lists\, trees\, etc . The decidability status of various fragments of the logic constitutes a long standing open problem. Current results report on techniques to decide satisfiability and validity of entailments for Separation Logic(s) over l ists (possibly with data). In this paper we establish a more general decid ability... DTSTART:20140318T154500 DTEND:20140318T174500 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Radu Iosif - The Tree Width of Separation Logic with Recursive Defi nitions END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6665h3HZLs@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = Seminar - Software Analysis - Tuesday 11 March 2014 - salle A. T uring CE4 = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = 15:45 - Salle : salle A. Turing CE4 Nicolas Halbwachs\, Verimag « Wh en the decreasing sequence fails... » Abstract: The classical method for pr ogram analysis by abstract interpretation\nconsists in computing a increas ing sequence with widening\, which\nconverges towards a correct solution\, then computing a decreasing\nsequence of correct solutions without wideni ng. It is generally\nadmitted that\, when the decreasing sequence reaches a fixpoint\,\nit cannot be improved further. As a consequence\, all effort s\nfor improving the precision of an analysis have been... DTSTART:20140311T154500 DTEND:20140311T174500 DURATION:PT2H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Nicolas Halbwachs - When the decreasing sequence fails... END:VEVENT BEGIN:VEVENT UID:20260705T081935UTC-6666a7meWr@129.88.40.24 DTSTAMP:20260705T081935Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 4 March 2014 - salle A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n15:45 - Salle : salle A. Turing CE4\n\nDavid Monniaux\, CNRS / VERIMAG\nhttp://www-verimag.imag.fr/~monniaux/\n\n« How to analyze arra ys by distinguishing only a couple of cells » \n\nAbstract:\n\nUsual stati c analysis approaches for programs handling arrays use special domains for representing sets of arrays\, or apply some form of pattern-based partiti oning to convert the array program into a scalar program. In our case\, we simply abstract the array a by one cell a[x]\, or two cells a[x] and a[y] \, with x