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:20201028T151635CET-8652FuIwRc@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8654OgHBcg@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8656S5xwa1@129.88.40.24
DTSTAMP:20201028T141635Z
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 ∃∗∀∗\, w
here the quantified 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:PT01H0M0S
LOCATION:206
SUMMARY:Cristina Serban - Reasoning in the Bernays-Schonfinkel-Ramsey Fragm
ent of Separation Logic
END:VEVENT
BEGIN:VEVENT
UID:20201028T151635CET-8658UpjcFT@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8660U38VHG@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8661aaXO7i@129.88.40.24
DTSTAMP:20201028T141635Z
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érieure
de Lyon\n\n\n« Using abstract interpretation on Horn clauses: arrays and
lists » \n\nAbstract:\n\nAutomatically verifying safety properties of pro
grams is a tough problem that has been tackled\nusing many different appro
aches: rewriting systems\, abstract interpretation\, SMT solving.\nMost te
chniques restrict themselves to programs operating on Boolean and integer
values and\ntransposing them to infinite data structures such as arrays ha
s not yet been satisfyingly achieved.\nRecent work by Monniaux and Gonnord
suggests to...
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:20201028T151635CET-8663z2cson@129.88.40.24
DTSTAMP:20201028T141635Z
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\n
https://www.normalesup.org/~truchet/\n\n« constraints programming & abstr
act interpretation » \n\nAbstract:\n\nFirst an introduction to constraint
s programming\, then relationship to abstract interpretation.\n\n\n= = = =
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\nOther
seminars at VERIMAG - http://www-verimag.imag.fr/Verimag-Seminars\,62.html
?lang=en\nHow to come to IMAG 206 - \nTo unsubscribe\, reply to this mail
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:20201028T151635CET-8664Uez7Bf@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8666XpaWiI@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-86687Gztvu@129.88.40.24
DTSTAMP:20201028T141635Z
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\, Écol
e des Mines de Nantes / LINA\nhttp://anicet.bart.free.fr/\n\n« Verifying
a Real-Time Language with Constraints » \n\nAbstract:\n\nFormal verificat
ion of real time programs\, where variables can be assigned different valu
es at every single time\, is difficult due to the analyses of loops with t
ime lags. In this talk\, we consider a problem arising from verification o
f real- time languages: checking of the range of stream variables. We pres
ent a constraint model for this problem\, and an algorithm\, combining con
straint...
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:20201028T151635CET-86695jsFrJ@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8671kALWd9@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8672e1g4cV@129.88.40.24
DTSTAMP:20201028T141635Z
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é\, CNR
S / ENS-Paris\nhttp://www.di.ens.fr/~mine/\n\n« tba » \n\nAbstract:\n\nt
ba\n\n\n= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
= = = =\nOther seminars at VERIMAG - http://www-verimag.imag.fr/Verimag-Se
minars\,62.html?lang=en\nHow to come to 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:20201028T151635CET-8674Z96n2B@129.88.40.24
DTSTAMP:20201028T141635Z
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=
= = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =\n
Other seminars at VERIMAG - http://www-verimag.imag.fr/Verimag-Seminars\,6
2.html?lang=en\nHow to come to salle A. Turing CE4 - http://www-verimag.im
ag.fr/Plan-d-acces.html?lang=fr\nTo unsubscribe\, reply to this mail 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:20201028T151635CET-8676EoFvWb@129.88.40.24
DTSTAMP:20201028T141635Z
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-Induction
with Continuously-Refined Invariants » \n\nAbstract:\n\nBounded model che
cking (BMC) is a well-known and successful technique for finding bugs in s
oftware.\n\nk-induction is an approach to extend BMC-based approaches from
falsification to verification.\n\nAutomatically generated auxiliary invar
iants can be used to strengthen\nthe induction hypothesis. We improve this
approach and further increase effectiveness and\nefficiency in the follow
ing way:...
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:20201028T151635CET-8677PbzUjo@129.88.40.24
DTSTAMP:20201028T141635Z
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 vulnerab
ility discovery using Machine Learning » \n\nAbstract:\n\nA typical OS us
ually involves thousands of executable files.\nFor these programs\, we can
have thousands of bugs reports. \nFuzzing and detecting vulnerabilities a
t the OS scale leads to\nnew issues and challenges. We think can address t
hese using\na combination of dynamic/static program analysis with Machine
Learning\ntechniques in order to learn pattern to discover vulnerable prog
rams\nand...
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:20201028T151635CET-8679n1rX4F@129.88.40.24
DTSTAMP:20201028T141635Z
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 wha
t if we look at this with a\ncompletely new perpective? The fundamental pr
oblem...
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:20201028T151635CET-86817hSwgU@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8682lZdFjz@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8684nVPFUM@129.88.40.24
DTSTAMP:20201028T141635Z
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 secu
red codes against control flow fault injections ) » \n\nRésumé :\n\nDa
ns le domaine des cartes à puces\, il est nécessaire de protéger les eq
uipements contre toutes attaques potentiellement dangereuses pour leur s
écurité. Les normes de développement de type Critères Communs exigent
d'effectuer...
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 symb
olic approach for evaluating the robustness of secured codes against cont
rol flow fault injections )
END:VEVENT
BEGIN:VEVENT
UID:20201028T151635CET-8685vmCsNU@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8688W0ww1U@129.88.40.24
DTSTAMP:20201028T141635Z
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:20201028T151635CET-8689J38Ngp@129.88.40.24
DTSTAMP:20201028T141635Z
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