BEGIN:VCALENDAR CALSCALE:GREGORIAN METHOD:PUBLISH PRODID:-//129.88.40.24//NONSGML iCalcreator 2.6// VERSION:2.0 SUMMARY:Software Verification Seminar X-WR-CALNAME:Software Verification Seminar X-WR-CALDESC:Software Verification Seminar X-WR-TIMEZONE:Europe/Paris BEGIN:VEVENT UID:20260405T231625CEST-2326sUtJ7r@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Thursday 27 April 2017 - Auditor ium (IMAG)\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n13:30 - Salle : Auditorium (IMAG)\n\nGeorge Karpenkov\, VERIM AG\nhttp://metaworld.me\n\n« Finding Inductive Invariants using SMT Solvi ng and Convex Optimization » \n\nAbstract:\n\nStatic analysis concerns it self with deriving program properties which hold\nuniversally for all prog ram executions.\nSuch properties are used for proving program properties ( e.g. there never\noccurs an overflow or other runtime error regardless of a particular execution) and are almost\ninvariably established using induc tive invariants: properties which hold\nfor the initial state and imply th emselves... DTSTART:20170427T133000 DTEND:20170427T153000 DURATION:PT02H0M0S LOCATION:Auditorium (IMAG) SUMMARY:George Karpenkov - Finding Inductive Invariants using SMT Solving a nd Convex Optimization END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2328vzKZsi@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Wednesday 22 March 2017 - Rm. 20 4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n13:30 - Salle : Rm. 204\n\nGeorge Karpenkov\, VERIMAG\nhttp://metaworl d.me\n\n« (PhD Defense Rehearsal): Finding Inductive Invariants using SMT Solving and Convex Optimization » \n\nAbstract:\n\nStatic analysis conce rns itself with deriving program properties which hold\nuniversally for al l program executions.\nSuch properties are used for proving program proper ties (e.g. there never\noccurs an overflow or other runtime error regardle ss of a particular execution) and are almost\ninvariably established using inductive invariants: properties which hold\nfor the initial state and im ply... DTSTART:20170322T133000 DTEND:20170322T150000 DURATION:PT01H30M0S LOCATION:Rm. 204 SUMMARY:George Karpenkov - (PhD Defense Rehearsal): Finding Inductive Invar iants using SMT Solving and Convex Optimization END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2329X3e9fW@129.88.40.24 DTSTAMP:20260405T211625Z 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 Bernays-Schonfinkel-Ramsey Fragment of Separation Logic » \n\nAbstract:\n \nSeparation Logic (SL) is a well-known assertion language used in Hoare-s tyle modular proof systems for programs with dynamically allocated data st ructures. In this paper we investigate the fragment of first-order SL rest rictedto the Bernays-Schonfinkel-Ramsey quantifier prefix ∃∗∀∗\, where the quantified variables range over the s et of memory locations. When this set is uninterpreted (has no associated theory) the fragment is... DTSTART:20170110T140000 DTEND:20170110T150000 DURATION:PT01H0M0S LOCATION:206 SUMMARY:Cristina Serban - Reasoning in the Bernays-Schonfinkel-Ramsey Fragm ent of Separation Logic END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-23299OPVKV@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Friday 4 November 2016 - Room 2 04\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n13:00 - Salle : Room 204\n\nGeorge Karpenkov\, VERIMAG\nhttp://metawo rld.me\n\n« Formula Slicing: Inductive Invariants from Preconditions » \n\nAbstract:\n\nWe propose a ``formula slicing'' method for finding induc tive invariants.\nIt is based on the observation that many loops in the pr ogram\naffect only a small part of the memory\,\nand many invariants which were valid before a loop are still valid after.\n\nGiven a precondition o f 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:PT01H0M0S LOCATION:Room 204 SUMMARY:George Karpenkov - Formula Slicing: Inductive Invariants from Preco nditions END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-23309iw0kH@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Friday 7 October 2016 - IMAG 20 6\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n14:00 - Salle : IMAG 206\n\nDavid Monniaux\, CNRS / VERIMAG\nhttp://ww w-verimag.imag.fr/~monniaux/\n\n« Cell morphing: from array programs to a rray-free Horn clauses » \n\nAbstract:\n\nAutomatically verifying safety properties of programs is hard. Many approaches exist for verifying\nprogr ams operating on Boolean and integer values (e.g. abstract interpretation\ , counterexample-guided\nabstraction refinement using interpolants)\, but transposing them to array properties has been fraught with difficulties. O ur work addresses that issue with a powerful and flexible abstraction\, pa rametric... DTSTART:20161007T140000 DTEND:20161007T150000 DURATION:PT01H0M0S LOCATION:IMAG 206 SUMMARY:David Monniaux - Cell morphing: from array programs to array-free H orn clauses END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-23317rNndu@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 14 June 2016 - IMAG 206 \n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n13:30 - Salle : IMAG 206\n\nJulien Braine\, École normale supérie ure de Lyon\n\n\n« Using abstract interpretation on Horn clauses: arrays and lists » \n\nAbstract:\n\nAutomatically verifying safety properties of programs is a tough problem that has been tackled\nusing many different a pproaches: rewriting systems\, abstract interpretation\, SMT solving.\nMos t techniques restrict themselves to programs operating on Boolean and inte ger values and\ntransposing them to infinite data structures such as array s has not yet been satisfyingly achieved.\nRecent work by Monniaux and Gon nord... DTSTART:20160614T133000 DTEND:20160614T143000 DURATION:PT01H0M0S LOCATION:IMAG 206 SUMMARY:Julien Braine - Using abstract interpretation on Horn clauses: arra ys and lists END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2331obK53O@129.88.40.24 DTSTAMP:20260405T211625Z 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 \nhttps://www.normalesup.org/~truchet/\n\n« constraints programming & abs tract interpretation » \n\nAbstract:\n\nFirst an introduction to constrai nts programming\, then relationship to abstract interpretation.\n\n\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nOthe r seminars at VERIMAG - http://www-verimag.imag.fr/Verimag-Seminars\,62.ht ml?lang=en\nLocation/Vision: IMAG 206 - \nTo unsubscribe\, reply to this m ail with UNSUBSCRIBE in the subject\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = =... DTSTART:20160607T140000 DTEND:20160607T150000 DURATION:PT01H0M0S LOCATION:IMAG 206 SUMMARY:Charlotte Truchet - constraints programming & abstract interpretati on END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2332bmt2po@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Wednesday 23 March 2016 - salle A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n14:00 - Salle : salle A. Turing CE4\n\nRadu Iosif\, Verima g\nhttp://nts.imag.fr/index.php/Radu_Iosif\n\n« Selected TACAS 2016 Paper s: a joint Software Analysis and Tempo seminar » \n\nAbstract:\n\nDogan U lus: Online Timed Pattern Matching\n\nTimed pattern matching consists in f inding all segments of a densetime\nBoolean signal that match a pattern de fined by a timed regular expression.\nThis problem has been formulated and solved in [17] via an offline algorithm that takes the signal and express ion as inputs and produces the set of all matches\, represented as a finit e union of... DTSTART:20160323T140000 DTEND:20160323T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Radu Iosif - Selected TACAS 2016 Papers: a joint Software Analysis and Tempo seminar END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2333BRaBjP@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Thursday 3 March 2016 - salle A . Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n15:00 - Salle : salle A. Turing CE4\n\nGeorge Karpenkov\, V ERIMAG\nhttp://metaworld.me\n\n« Introduction to SMT & JavaSMT: A Unified Library for Utilizing SMT Solvers » \n\nAbstract:\n\nThe talk is split i n two short parts.\nThe first part is by David Monniaux.\n\nDavid will giv e an introduction to satisfiability modulo theory:\n- what it is\n- how so lvers are used\n- usual theories\n- limitations\n\nThe second part is by G eorge Karpenkov.\nGeorge will give a short talk on the newly developed Jav aSMT 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:20260405T231625CEST-2334l6T3Gk@129.88.40.24 DTSTAMP:20260405T211625Z 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\, Éc ole des Mines de Nantes / LINA\nhttp://anicet.bart.free.fr/\n\n« Verifyin g a Real-Time Language with Constraints » \n\nAbstract:\n\nFormal verific ation of real time programs\, where variables can be assigned different va lues 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 real- time languages: checking of the range of stream variables. We pr esent a constraint model for this problem\, and an algorithm\, combining c onstraint... DTSTART:20151207T140000 DTEND:20151207T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Anicet Bart - Verifying a Real-Time Language with Constraints END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2334gvwDhv@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Thursday 26 February 2015 - sall e A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n14:00 - Salle : salle A. Turing CE4\n\nGeorge Karpenkov\ , VERIMAG\n\n\n« Scalable Code Analysis with Policy Iteration » \n\nAbst ract:\n\nWe present a new algorithm for deriving numerical invariants\nwhi ch combines the precision of max-policy iteration with the flexibility\nan d scalability of conventional Kleene iterations.\nIt is stated using Confi gurable Program Analysis\nframework\, thus allowing inter-analysis communi cation.\nWe augment the algorithm with adjustable block encoding\, which g ives better\nresults than the existing path focusing approach\, and with a novel... DTSTART:20150226T140000 DTEND:20150226T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:George Karpenkov - Scalable Code Analysis with Policy Iteration END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2335J4VL6U@129.88.40.24 DTSTAMP:20260405T211625Z 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 Separation Logic with Tree Automata » \n\nAbstract:\n\nSeparation Logic ( SL) with inductive definitions is a natural formalism for specifying compl ex recursive data structures\, used in compositional verification of progr ams manipulating such structures. The key ingredient of any automated veri fication procedure based on SL is the decidability of the entailment probl em. In this work\, we reduce the entailment problem for a non-trivial subs et of SL... DTSTART:20141217T140000 DTEND:20141217T160000 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Radu IOSIF - Deciding Entailments in Inductive Separation Logic wit h Tree Automata END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2336uXTJPE@129.88.40.24 DTSTAMP:20260405T211625Z 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é\, C NRS / 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 -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 t his mail 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:20260405T231625CEST-2349BW95TZ@129.88.40.24 DTSTAMP:20260405T211625Z 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\nExp osé du stage de Dorian Nogneng à University of Western Ontario.\n\n \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:20140909T143000 DTEND:20140909T153000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Dorian Nogneng - fonctions de Schur END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2350eviIgT@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Friday 6 June 2014 - salle A. T uring CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n14:00 - Salle : salle A. Turing CE4\n\nPhilipp Wendler\, Unive rsität Passau\nhttp://www.philippwendler.de/\n\n« Combining k-Inductio n with Continuously-Refined Invariants » \n\nAbstract:\n\nBounded model c hecking (BMC) is a well-known and successful technique for finding bugs in software.\n\nk-induction is an approach to extend BMC-based approaches fr om falsification to verification.\n\nAutomatically generated auxiliary inv ariants can be used to strengthen\nthe induction hypothesis. We improve th is approach and further increase effectiveness and\nefficiency in the foll owing... DTSTART:20140606T140000 DTEND:20140606T150000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Philipp Wendler - Combining k-Induction with Continuously-Refined I nvariants END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2351eafP0V@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Monday 2 June 2014 - salle A. T uring CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n15:30 - Salle : salle A. Turing CE4\n\nGustavo Grieco\, Univer sité de Rosario (Argentina) et Verimag\n\n\n« On some ideas for vulner ability discovery using Machine Learning » \n\nAbstract:\n\nA typical OS usually involves thousands of executable files.\nFor these programs\, we c an have thousands of bugs reports. \nFuzzing and detecting vulnerabilities at the OS scale leads to\nnew issues and challenges. We think can address these using\na combination of dynamic/static program analysis with Machin e Learning\ntechniques in order to learn pattern to discover vulnerable... DTSTART:20140602T153000 DTEND:20140602T163000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Gustavo Grieco - On some ideas for vulnerability discovery using Ma chine Learning END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2351ZjDjlz@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 13 May 2014 - salle A. T uring CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n15:30 - Salle : salle A. Turing CE4\n\nSudakshina Das\, Oxford University\n\n\n« Significance of Liveness based approach to Pointer Ana lysis » \n\nAbstract:\n\nA flow and context sensitive pointer analysis is known to be very precise but is also\ninfamous to be highly inefficient. Almost all approaches to pointer analysis are done with\napproximations th at is with either flow or context sensitivity but seldom with both. In fac t\nGCC’s pointer analysis pass ′ pta ′ is done with neither . But what if we look at this with a\ncompletely new perpective? The funda mental... DTSTART:20140513T153000 DTEND:20140513T163000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Sudakshina Das - Significance of Liveness based approach to Pointer Analysis END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-23523ugvz8@129.88.40.24 DTSTAMP:20260405T211625Z 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 In variant Generation using Logic-based Automatic Abstract Transformers » \n \nAbstract:\n\nFormal analysis tools for system models often require or be nefit from the availability of auxiliary system invariants. Abstract inter pretation is currently one of the best approaches for discovering useful i nvariants\, in particular numerical ones. However\, its application is lim ited by two orthogonal issues: (i) developing an abstract interpretation i s often... DTSTART:20140414T150000 DTEND:20140414T160000 DURATION:PT01H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Cesare Tinelli - Incremental Invariant Generation using Logic-based Automatic Abstract Transformers END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2353EVoJ91@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Monday 31 March 2014 - salle A. Pnueli CE3\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n14:30 - Salle : salle A. Pnueli CE3\n\nFrancesco Alberti\, Un iversity of Lugano and VERIMAG\nhttp://www.inf.usi.ch/phd/alberti/\n\n« D ecision Procedures for Flat Array Properties » \n\nAbstract:\n\nWe presen t new decidability results for quantified fragments of theories of arrays. \nOur decision procedures are fully declarative\, parametric in the theori es of indexes and elements and orthogonal with respect to known results.\n We also discuss applications to the analysis of programs handling arrays. \nThis is a joint work with S. Ghilardi and N. Sharygina\n\n\n= = = = = = = = = = = = =... DTSTART:20140331T143000 DTEND:20140331T153000 DURATION:PT01H0M0S LOCATION:salle A. Pnueli CE3 SUMMARY:Francesco Alberti - Decision Procedures for Flat Array Properties END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2353zfmwJk@129.88.40.24 DTSTAMP:20260405T211625Z 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 symb olique pour évaluer la robustesse d'un code aux attaques par injection de fautes (Lazart: a symbolic approach for evaluating the robustness of se cured codes against control flow fault injections ) » \n\nRésumé :\n\n Dans le domaine des cartes à puces\, il est nécessaire de protége r les equipements contre toutes attaques potentiellement dangereuses pour leur sécurité. Les normes de développement de type Critères Co mmuns... DTSTART:20140325T154500 DTEND:20140325T164500 DURATION:PT01H0M0S 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 sy mbolic approach for evaluating the robustness of secured codes against co ntrol flow fault injections ) END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2354iKNDis@129.88.40.24 DTSTAMP:20260405T211625Z 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 describin g dynamically allocated linked data structures\, such as lists\, trees\, e tc. The decidability status of various fragments of the logic constitutes a long standing open problem. Current results report on techniques to deci de satisfiability and validity of entailments for Separation Logic(s) over lists (possibly with data). In this paper we establish a more general dec idability... DTSTART:20140318T154500 DTEND:20140318T174500 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Radu Iosif - The Tree Width of Separation Logic with Recursive Defi nitions END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-2355MHU9fP@129.88.40.24 DTSTAMP:20260405T211625Z CATEGORIES:Soft_sem DESCRIPTION:= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nSeminar - Software Analysis - Tuesday 11 March 2014 - salle A. Turing CE4\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n15:45 - Salle : salle A. Turing CE4\n\nNicolas Halbwachs\, V erimag\n\n\n« When the decreasing sequence fails... » \n\nAbstract:\n\nT he classical method for program analysis by abstract interpretation\nconsi sts in computing a increasing sequence with widening\, which\nconverges to wards a correct solution\, then computing a decreasing\nsequence of correc t solutions without widening. It is generally\nadmitted that\, when the de creasing sequence reaches a fixpoint\,\nit cannot be improved further. As a consequence\, all efforts\nfor improving the precision of an analysis ha ve been... DTSTART:20140311T154500 DTEND:20140311T174500 DURATION:PT02H0M0S LOCATION:salle A. Turing CE4 SUMMARY:Nicolas Halbwachs - When the decreasing sequence fails... END:VEVENT BEGIN:VEVENT UID:20260405T231625CEST-23567Co4Iv@129.88.40.24 DTSTAMP:20260405T211625Z 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 arr ays by distinguishing only a couple of cells » \n\nAbstract:\n\nUsual sta tic analysis approaches for programs handling arrays use special domains f or representing sets of arrays\, or apply some form of pattern-based parti tioning 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