BEGIN:VCALENDAR
PRODID:-//Inverse inc./SOGo 2.3.23//EN
VERSION:2.0
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:Europe/Berlin
X-LIC-LOCATION:Europe/Berlin
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:100D-5760FA00-1-4D2CF380
SUMMARY:Sanjiva Prasad: From ABC to a LitTLe logic for mobile networks
LOCATION:TUM MI 03.09.014
DESCRIPTION:We revisit the model of Abstract Switches presented in the axio
matic basis for communication (ABC) proposed by Karsten et al (SIGCOMM 200
7)\, to examine networks whose routing behaviour can vary over time\, ref
ormulating the axioms using temporal logic.\n\nIn this framework\, we exam
ine the essence of the IPv6 protocol\, a quintessential model of mobility\
, presenting a new proof of its correctness\, i.e\, that if a mobile node
s remains stationed at a host ``long enough’’\, data messages addressed to
it will eventually get delivered (TGC 2015). \n\nWe then show how this c
orrectness of IPv6 (a liveness property) can be established by model-check
ing a bounded liveness property on a small model\, and using parametric ve
rification techniques. This approach can be applied to IPv6 since the sys
tem eventually converges to a ``stable’' subsystem (HVC 2015).
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160615T064717Z
DTSTAMP:20160615T064717Z
LAST-MODIFIED:20160620T132217Z
DTSTART;TZID=Europe/Berlin:20160624T090000
DTEND;TZID=Europe/Berlin:20160624T100000
TRANSP:OPAQUE
SEQUENCE:2
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:103B-5588FB00-13-1C6382
SUMMARY:Martin Hofmann: The groupoid interpretation of type theory -- a per
sonal retrospective
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150623T062317Z
DTSTAMP:20150623T062317Z
LAST-MODIFIED:20150715T092324Z
DTSTART;TZID=Europe/Berlin:20150717T083000
DTEND;TZID=Europe/Berlin:20150717T093000
TRANSP:OPAQUE
LOCATION:LMU D Z007
SEQUENCE:1
DESCRIPTION:This will essentially be the same as my invited talk at TLCA'15
in Warsaw\, 3rd July 2015\n\nBack in 1994 Thomas Streicher and myself dis
covered the groupoid interpretation of Martin-Löf's type theory which is n
ow seen as a precursor of Homotopy Type Theory and in fact anticipated som
e simple cases of important ideas of Homotopy Type Theory\, notably a spec
ial case of the univalence axiom. I will explain how and why we found the
groupoid interpretation\, our motivations and results. I will also try to
give an informed outsider's view of Homotopy Type Theory as it is today an
d finally give a glance at a novel application of the groupoid interpretat
ion in the context of denotational semantics (proof-relevant logical rela
tions).\n
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150940PQA@lapbroy149
DTSTART;TZID=Europe/Berlin:20110202T170000
DTEND;TZID=Europe/Berlin:20110202T180000
SUMMARY:Perst Thomas: Banking IT or how to run a changing system
DESCRIPTION:With the subprime crisis of 2007 it became clear that financial
institutions have to steer their risks with sophisticated methods on the
basis of consolidated information about the managed business. This require
ment has to be supported by an integrative and robust IT architecture whic
h can smoothly react on a change in the business strategy. The talk will p
resent risk steering methods\, modelling techniques\, and IT strategies to
face the challenges of modern banking.
LOCATION:TUM Garching\, Room 02.07.014
CONTACT:Perst Thomas
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150941abw@lapbroy149
DTSTART;TZID=Europe/Berlin:20111021T083000
DTEND;TZID=Europe/Berlin:20111021T093000
SUMMARY:Fisher Jasmin: Model Checking Cell Fate Decisions
DESCRIPTION:As time goes by\, it becomes more and more apparent that the pu
zzles of life involve more and more molecular pieces that fit together in
increasingly complex ways. Biology is not an exact science. It is messy an
d noisy\, and most often vague and ambiguous. We cannot assign clear rules
to the way cells behave and interact with one another. And we often canno
t quantify the exact amounts of molecules\, such as genes and proteins\, i
n the resolution of a single cell. To make matters worse (so to speak)\, t
he combinatorial complexity observed in biological networks is staggering\
, which renders the comprehension and analysis of such systems a major cha
llenge. Recent efforts to create executable models of complex biological p
henomena - an approach called Executable Biology - entail great promise fo
r new scientific discoveries\, shading new light on the puzzle of life. At
the same time\, this 'new wave of the future' forces computer science to
stretch far and beyond\, and in ways never considered before\, in order to
deal with the enormous complexity observed in biology. In this talk\, I w
ill summarize some of the success stories in using formal verification to
reason about mechanistic models in biology. In particular\, I will focus o
n models of cell fate decisions during development and cancer\, and their
analysis using model checking.\n \nJoint work with: Nir Piterman\, David H
arel\, Tom Henzinger\, Byron Cook\, Moshe Vardi\, Freddy Radtke\, and Alex
Hajnal.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Fisher Jasmin
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150942aZJ@lapbroy149
DTSTART;TZID=Europe/Berlin:20120224T100000
DTEND;TZID=Europe/Berlin:20120224T110000
SUMMARY:Traytel Dmitriy: Extending Hindley-Milner Type Inference with Coerc
ive Structural Subtyping
DESCRIPTION:Coercions allow to convert between different types\, and their
automatic\ninsertion can greatly increase readability of terms. We present
\na type inference algorithm that\, given a term without type information\
,\ncomputes a type assignment and determines at which positions in the\nte
rm coercions have to be inserted to make it type-correct according to\nthe
standard Hindley-Milner system (without any subtypes). The algo-\nrithm i
s sound and\, if the subtype relation on base types is a disjoint\nunion o
f lattices\, also complete. The algorithm is used in the proof\nassistant
Isabelle.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Traytel Dmitriy
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150943t2n@lapbroy149
DTSTART;TZID=Europe/Berlin:20130830T100000
DTEND;TZID=Europe/Berlin:20130830T110000
SUMMARY:Losa Giuliano: Reasoning about adaptive distributed algorithms
DESCRIPTION:To reach practical performance\, distributed algorithm must dyn
amically\nadapt to their environment (faults\, asynchrony\, load\, content
ion...).\nAdaptive distributed algorithms often achieve dynamic adaptation
by\nswitching between several modes\, each mode being a complex algorithm
on\nits own. The interaction between modes presents a challenge to formal
\nverification. Indeed\, we do not know of any formally verified adaptive\
ndistributed algorithm.\nWe present a framework in which each mode of an a
daptive distributed\nalgorithm can be specified and verified independently
of the other\nmodes. We demonstrate that our framework enables verifying
adaptive\ndistributed algorithms using several examples formalized in TLA
and\nIsabelle/HOL.
LOCATION:TUM Informatik - room 00.09.038 (Garching)
CONTACT:Losa Giuliano
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:139151509440Ko@lapbroy149
DTSTART;TZID=Europe/Berlin:20121109T100000
DTEND;TZID=Europe/Berlin:20121109T110000
SUMMARY:Martin Hofmann: Tutorial on type and effect systems
LOCATION:Garching\, MI 02.07.014.
CONTACT:Martin Hofmann
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:139151509441dS@lapbroy149
DTSTART;TZID=Europe/Berlin:20100514T083000
DTEND;TZID=Europe/Berlin:20100514T093000
SUMMARY:Brauer Joerg: Automatic Abstraction for Intervals using Boolean For
mulae
DESCRIPTION:Traditionally\, transfer functions have been manually designed
for each\noperation in a program. Recently\, however\, there has been grow
ing\ninterest in computing transfer functions\, motivated by the desire to
\nreason about sequences of operations that constitute basic blocks.\n\nOu
r work focuses on deriving transfer functions for intervals â?? possibly\n
the most widely used numeric domain â?? and shows how they can be\ncompute
d from Boolean formulae which are derived through\nbit-blasting. This appr
oach is entirely automatic\, avoids complicated\nelimination algorithms\,
and provides a systematic way of handling\nwrap-arounds (integer overflows
and underflows) which arise in\nmachine arithmetic.
LOCATION:LMU Main Building - A 011
CONTACT:Brauer Joerg
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:139151509446V@lapbroy149
DTSTART;TZID=Europe/Berlin:20131118T160000
DTEND;TZID=Europe/Berlin:20131118T170000
SUMMARY:Mueller Christian: Modular Interprocedural Verification using Inter
polant Function Summaries
DESCRIPTION:When model checking large software projects\, one has to deal w
ith the\nstate space explosion problem. This means we have to rely on fini
te abstractions of the state space that can be refined gradually.\nTo be a
ble to reason efficiently about interprocedural traces\, it is\nneccessary
to abstract away function calls and reuse information on every\ncall site
. This can be accomplished by using Function Summaries\, which\nshould be
refinable\, reusable and only be computed as needed.\n\nIn this thesis\, w
e propose a novel algorithm that uses an SMT-Solver to\ncompute Interpolan
t Function Summaries which can be refined on demand\,\nreused in every cal
ling context\, and eliminate the need to inline other\nfunctions.\nWe will
show how this can be used to augment the concept of Trace\nRefinement and
find considerable improvements when dealing with function\ncalls.
LOCATION:TUM Garching - 02.07.014
URL:http://www.model.in.tum.de/~frieling/2013-11-18-Christian-Mueller.pdf
CONTACT:Mueller Christian
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:139151509447cS@lapbroy149
DTSTART;TZID=Europe/Berlin:20130111T100000
DTEND;TZID=Europe/Berlin:20130111T110000
SUMMARY:Zimmerman Martin: Cost-Parity Games and Cost-Streett Games\n
DESCRIPTION:We consider two-player games played on finite graphs with costs
on edges\nand introduce two wining conditions\, cost-parity and cost-Stre
ett\, which\nrequire bounds on the costs between requests and their respon
ses.\n\nFor cost-parity games we show that the first player has positional
winning\nstrategies and that determining the winner lies in NP intersecti
on co-NP.\nFor cost-Street games we show that the first player has finite-
state\nwinning strategies and that determining the winner is EXPTIME-compl
ete.
LOCATION:Garching MI 02.07.014
CONTACT:Zimmerman Martin
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150944xKQ@lapbroy149
DTSTART;TZID=Europe/Berlin:20120120T083000
DTEND;TZID=Europe/Berlin:20120120T093000
SUMMARY:Katoen Joost-Pieter: Formal Verification and Performability Analysi
s in the Aerospace Domain: An Experience Report
DESCRIPTION:The engineering process of on-board critical embedded systems i
nvolves a wide range of diverse approaches and techniques for system-level
aspects such as functional correctness\, dependability and safety\, as we
ll as \nperformance. Establishing these properties in a trustworthy manne
r is a highly challenging task. This is severely complicated by the heter
ogeneous character of on-board systems involving software\, sensors\, actu
ators\, electrical components\, etc.\, that each has its own specific deve
lopment approach supported by different modeling and analysis techniques.\
n\nIn this talk\, we will report on a serious attempt to develop an integr
ated approach for all aforementioned aspects. The key is a general-purpose
modeling and specification formalism based on AADL\, enriched with a\nric
h palette of formal analysis techniques for all properties and measures of
interest. It is supported by an advanced toolset which is centered aroun
d state-of-the-art symbolic and stochastic model checking. We present our
AADL dialect\, its formal semantics\, its main analysis features\, and th
e extensive evaluation of our approach in an industrial context.\n\n(The w
ork has been conducted in the context of several projects that are funded
by the European Space Agency.)
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Katoen Joost-Pieter
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150945PWi@lapbroy149
DTSTART;TZID=Europe/Berlin:20120525T083000
DTEND;TZID=Europe/Berlin:20120525T093000
SUMMARY:Kramer Simon: A Logic of Interactive Proofs (Formal Theory of Knowl
edge Transfer)
DESCRIPTION:We propose a logic of interactive proofs as the first and main
step towards an intuitionistic foundation for interactive computation to b
e obtained via an interactive analog of the G\\odel-Kolmogorov-Art\\\\emov
definition of intuitionistic logic as embedded into a classical modal log
ic of proofs\, and of the Curry-Howard isomorphism between intuitionistic
proofs and typed programs. Our interactive proofs effectuate a persistent
epistemic impact in their intended communities of peer reviewers that cons
ists in the induction of the (propositional) knowledge of their proof goal
by means of the (individual) knowledge of the proof with the interpreting
reviewer. That is\, interactive proofs effectuate a transfer of propositi
onal knowledge (knowable facts) via the transfer of certain individual kno
wledge (knowable proofs) in distributed and multi-agent systems. In other
words\, we as a community can have the formal common knowledge that a proo
f is that which if known to one of our peer members would induce the knowl
edge of its proof goal with that member.
LOCATION:tba.
CONTACT:Kramer Simon
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150945rrJ@lapbroy149
DTSTART;TZID=Europe/Berlin:20101126T100000
DTEND;TZID=Europe/Berlin:20101126T110000
SUMMARY:Kostic\n Dejan: Predicting Faults in Heterogeneous\, Federated Dist
ributed Systems
DESCRIPTION:Abstract:\n\nIt is notoriously difficult to make distributed sy
stems reliable. This becomes\neven harder in the case of the widely-deploy
ed systems that become\nheterogeneous and federated. The set of routers in
charge of the inter-domain\nrouting in the Internet is a prime example of
such a system. The unanticipated\ninteraction of nodes under seemingly va
lid configuration changes and local\nfault-handling can have a profound ef
fect. For example\, the Internet has\nsuffered from multiple IP prefix hij
ackings\, as well as performance and\nreliability problems due to emergent
behavior resulting from a local session\nreset. \n\nWe argue that the key
step in making these systems reliable is the need to\nautomatically predi
ct faults. In this talk\, I will describe the design and\nimplementation o
f DiCE\, a system that uses temporal and spatial awareness to\npredict fau
lts in heterogeneous\, federated systems. Our live evaluation in the\ntest
bed shows that DiCE quickly and successfully predicts two important classe
s\nof faults\, operator mistakes and programming errors\, that have plague
d BGP\nrouting in the Internet.\n\nJoint work with Marco Canini\, Vojin Jo
vanovic\, Gautam Kumar\, Boris Spasojevic\,\nand Olivier Crameri\n\nBio:\n
\nDejan Kosti? obtained his Ph.D. in Computer Science at the Duke Universi
ty\,\nunder Amin Vahdat. He spent the last two years of his studies and a
brief stay\nas a postdoctoral scholar at the University of California\, Sa
n Diego. He\nreceived his Master of Science degree in Computer Science fro
m the University\nof Texas at Dallas\, and his Bachelor of Science degree
in Computer Engineering\nand Information Technology from the University of
Belgrade (ETF)\, Serbia. In\nJanuary 2006\, he started as a tenure-track
assistant professor at the School of\nComputer and Communications Sciences
at EPFL (Ecole Polytechnique FÃ©dÃ©rale de\nLausanne)\, Switzerland. In 2
010\, he received a European Research Council (ERC)\nStarting Investigator
Award. His interests include Distributed Systems\,\nComputer Networks\, O
perating Systems\, and Mobile Computing.
LOCATION:TUM Garching\, Room 03.09.014\n
CONTACT:Kostic\n Dejan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:139151509464iy@lapbroy149
DTSTART;TZID=Europe/Berlin:20100718T083000
DTEND;TZID=Europe/Berlin:20100718T093000
SUMMARY:Seidl Helmut: Fancy fixpoint algorithms for interprocedurally analy
zing dataraces
LOCATION:LMU Main Building - A 011
CONTACT:Seidl Helmut
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:139151509466wc@lapbroy149
DTSTART;TZID=Europe/Berlin:20110513T083000
DTEND;TZID=Europe/Berlin:20110513T093000
SUMMARY:Maffei\n Matteo: Formal Methods for the Design and Verification of
Cryptographic\nApplications
DESCRIPTION:Designing security protocols is notoriously error-prone and\nse
curity proofs of such protocols are awkward for\nhumans. Several technique
s based on formal methods were recently\nproposed to automate protocol ana
lysis. Despite these promising\nresults\, the design and verification of m
odern cryptographic\napplications is still an open issue. First\, the desi
gn of\ncryptographic protocols is driven by best practices and human\nexpe
rtise and there exist virtually no techniques to automate this\ntask. Seco
nd\, modern protocols rely on complex cryptographic\nprimitives and achiev
e sophisticated security properties that are\nmostly not supported by exis
ting verification tools. Finally\, current\nautomated analysis techniques
do not provide end-to-end security\nguarantees\, since they focus on the l
ogic of the protocol and tend to\nabstract away from its implementation.\n
\n\nIn this talk\, I will present some recent work on formal methods for\n
the design and verification of cryptographic applications. I will\nfocus\,
in particular\, on two fundamental\, and seemingly contradictory\,\nprope
rties in the design of secure systems\, namely\, authorization and\nprivac
y. On the one hand\, the access to sensitive resources should be\ngranted
only to authorized users\; on the other hand\, these users would\nlike to
share as little personal information as possible with third\nparties.\n\nI
will present a framework for the specification and\nenforcement of privac
y-aware authorization policies in decentralized\nsystems. These policies\n
are specified as a set of logical rules\, in which the traditional says\nm
odality from authorization logics is accompanied by existential\nquantific
ation in order to express the secrecy of sensitive\ninformation. The real
ization of these policies is obtained by a\npowerful combination of digita
l signatures and zero-knowledge\nproofs. We developed a compiler to automa
tically generate\ncryptographic implementations (i.e.\,\ncryptographic li
brary and source code) from high-level logical\nspecifications. The secur
ity of these implementations is enforced\nby a type system based on refin
ement\, union\, and intersection types.
LOCATION:LMU Main Building - A U117
CONTACT:Maffei\n Matteo
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:139151509477yT@lapbroy149
DTSTART;TZID=Europe/Berlin:20100129T141500
DTEND;TZID=Europe/Berlin:20100129T151500
SUMMARY:Hofmann Martin: What is a pure functional?
DESCRIPTION:We investigate the following question. Given a higher-order SML
function\n\nÂ Â Â Â Â Â Â Â Â Â Â Â Â Â Â Â Â Â Â Â F : (int->int) -> int
\n\nhow can we rigorously specify that F is pure\, ie produces no side-eff
ects\nother than those arising from calling its functional argument.\n(If
you don't like higher-order SML functions think of F as a method that\nmay
invoke a library function. It should produce no side-effects other\nthan
those that might arise from calls to the library function.)\n\nWe show tha
t existing methods based on preservation of invariants and\nrelational par
ametricity are insufficient for this purpose and thus define\na new notion
that captures purity in the sense that for any functional F\nthat is pure
in this sense there exists a corresponding question-answer\nstrategy\, ie
an element of the datatype\n\ntype tree = Answer of int | Question of int
* (int -> tree)\n\nThis work is motivated by the ongoing effort to verify
a new fixpoint\nalgorithm by Helmut Seidl which takes such a functional a
s input (or\nrather a functional of type ((Variables->Domain)->(Variables-
>Domain)) and\nwhose correctness is contingent on this functional to be pu
re.\n
LOCATION:LMU Oettingerstr. 67\, L109
CONTACT:Hofmann Martin
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150947c0T@lapbroy149
DTSTART;TZID=Europe/Berlin:20100712T140000
DTEND;TZID=Europe/Berlin:20100712T150000
SUMMARY:Hack Sebastian: Instruction Selection by Partitioned Boolean Quadra
tic Programming (PBQP)
DESCRIPTION:Since long\, instruction selection for expression trees is well
\nunderstood and efficient algorithms exist based on dynamic programming\,
\npossibly compiled into tree automata. Modern compilers\, however\, rely
on\ngraph-based program representations where instruction selection is NP-
hard.\n\nIn this talk we present a formulation of instruction selection by
PBQP and\nshow how the resulting instances occurring in practice can be s
olved efficiently.
LOCATION:TUM Garching\, 02.07.014
CONTACT:Hack Sebastian
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150947k6b@lapbroy149
DTSTART;TZID=Europe/Berlin:20100510T160000
DTEND;TZID=Europe/Berlin:20100510T170000
SUMMARY:Avigad Jeremy: Decision procedures\, heuristic procedures\, and for
mally verified mathematics
DESCRIPTION:I will describe a mixed-bag of decidability results\, some prac
tical\, and some not\, loosely related to problems that arise in the forma
l verification of mathematics. First\, I will discuss a decision procedure
for a fragment of a theory of asymptotic big O equations. Next\, I will d
iscuss Nelson-Oppen combination methods in the context of theories of the
real numbers. Finally\, I will discuss the geometric proofs one finds in E
uclid's *Elements*\, and procedures that read information off from the dia
gram.\n(These various projects involve joint work with Ed Dean\, Kevin Don
nelly\, Harvey Friedman\, and John Mumma).
LOCATION:TUM Garching\, 01.09.014
CONTACT:Avigad Jeremy
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150948GoR@lapbroy149
DTSTART;TZID=Europe/Berlin:20131129T100000
DTEND;TZID=Europe/Berlin:20131129T110000
SUMMARY:Kretinsky Jan: Some recent advances in probabilistic model checking
DESCRIPTION:Many probabilistic systems ranging from protocols to medical de
vices\ncan be\nmodelled as Markov decision processes (MDP).\nAlthough the
analysis of finite-state MDPs has proved useful and practical\nin many cas
es\, it is still impossible to verify complex properties or\nMDPswith huge
state spaces. We show some approaches tackling these\nproblems in\nthe re
cent 3 years. Firstly\, for checking more complex properties\, we show\nho
w to encode them in automata efficiently so that the product of the\nMDPan
d the automaton is smaller and faster to analyze. Secondly\, for\nhuge\nMD
Ps\, one can employ statistical model checking based on simulations and\nm
achine learning methods. These approaches have already led to speed\nups i
n\norders of magnitude\, but still offer plenty of open questions and\npos
sibilities for vast improvements.
LOCATION:TUM Garching - 02.07.014
URL:http://www.model.in.tum.de/~frieling/2013-11-29-Jan-Kretinsky.pdf
CONTACT:Kretinsky Jan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150948IIZ@lapbroy149
DTSTART;TZID=Europe/Berlin:20090115T160000
DTEND;TZID=Europe/Berlin:20090115T170000
SUMMARY:Sutcliffe Geoff: TPTP\, TSTP\, CASC\, etc. - Automated Reasoning in
Practice
DESCRIPTION:This talk gives an overview of activities and products that ste
m from the Thousands of Problems for Theorem Provers (TPTP) problem librar
y for Automated Theorem Proving (ATP) systems. These include the TPTP itse
lf\, the Thousands of Solutions from Theorem Provers (TSTP) solution libra
ry\, the TPTP language\, the CADE ATP System Competition (CASC)\, tools su
ch as my semantic Derivation Verifier (GDV) and the Interactive Derivation
Viewer (IDV)\, meta-ATP systems such as the Smart Selective Competition P
arallelism (SSCPA) system and the Semantic Relevance Axiom Selection Syste
m (SRASS)\, online access to automated reasoning systems and tools through
the SystemOnTPTP web service\, and applications in various domains. Curre
nt work extending the TPTP to higher-order logic will be introduced.
LOCATION:Garching\, room MI 01.11.018
CONTACT:Sutcliffe Geoff
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150948ITk@lapbroy149
DTSTART;TZID=Europe/Berlin:20131205T160000
DTEND;TZID=Europe/Berlin:20131205T170000
SUMMARY:Middeldorp Aart: Beyond Peano Arithmetic - Automatically Proving Te
rmination of the Goodstein Sequence
DESCRIPTION:Kirby and Paris (1982) proved in a celebrated paper that a theo
rem\nof Goodstein (1944) cannot be established in Peano (1889) arithmetic.
\nWe present an encoding of Goodstein's theorem as a termination problem\n
of a finite rewrite system. Using a novel implementation of ordinal\ninter
pretations\, we are able to automatically prove termination of\nthis syste
m\, resulting in the first automatic termination proof for\na system whose
derivational complexity is not multiply recursive.\nIn this talk\, which
is based on joint work with Sarah Winkler and\nHarald Zankl\, we also disc
uss the challenges when implementing the\nelementary interpretations of Le
scanne (1995).
LOCATION:TUM Garching - Room 00.09.038
URL:http://www.model.in.tum.de/~frieling/2013-12-05-Aart-Middeldorp.pdf
CONTACT:Middeldorp\n Aart
LAST-MODIFIED:20140313T141027Z
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:139151509496jv@lapbroy149
DTSTART;TZID=Europe/Berlin:20130717T140000
DTEND;TZID=Europe/Berlin:20130717T150000
SUMMARY:Avigad Jeremy: Dirichlet's theorem and the evolution of higher-orde
r reasoning in mathematics
DESCRIPTION:In 1837\, Peter Gustav Lejeune Dirichlet proved that there are
infinitely many\nprimes in any arithmetic progression in which the terms d
o not all have a common\nfactor. This beautiful and important result was s
eminal in the use of analytic\nmethods in number theory.\n\nContemporary p
resentations of Dirichlet's proof are manifestly higher-order. To\nprove t
he theorem for an arithmetic progression with common difference k\, one\nc
onsiders the set of Dirichlet characters modulo k\\\, which are certain ty
pes of\nfunctions from the integers to the complex numbers. One defines th
e Dirichlet\\nL-series L(s\, chi)\, where s is a complex number and chi is
a character modulo\nk. One then sums certain expressions involving the L-
series over the set of\ncharacters.\n\nThis way of thinking about characte
rs\, which involves treating functions as\nobjects just like the natural n
umbers\, was not available in the middle of the\nnineteenth century. Subse
quent presentations of Dirichlet's theorem from\nDedekind to Landau show a
gradual evolution towards the contemporary viewpoint\,\nshedding light on
the development of modern mathematical method.
LOCATION:Garching MI 00.09.038
CONTACT:Avigad\n Jeremy
LAST-MODIFIED:20140313T141104Z
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:13915150949zfr@lapbroy149
DTSTART;TZID=Europe/Berlin:20110121T100000
DTEND;TZID=Europe/Berlin:20110121T110000
SUMMARY:Chakraborty Samarjit: Automata-theoretic Modeling of Streaming Appl
ications
DESCRIPTION:Lately\, there has been a considerable amount of interest in de
sign\nmethodologies for embedded systems that are specifically targeted\nt
owards stream processing\, e.g.\, audio/video applications and control\nap
plications processing sensor data. Streams processed by such\napplications
tend to be highly bursty and exhibit a high\ndata-dependent variability i
n their processing requirements. As a\nresult\, classical event and servic
e models such as periodic\, sporadic\,\netc. can be overly pessimistic whe
n dealing with such applications. In\nthis talk I will discuss some of our
recent work on using\nautomata-theoretic models for this domain. In parti
cular\, I will\npresent a new model called Event Count Automata for captur
ing the\ntiming properties and execution requirements of irregular/bursty\
nstreams. This model can be used to cleanly formulate properties\nrelevant
to stream processing on heterogeneous multiprocessor\narchitectures\, suc
h as buffer overflow/underflow constraints. Apart\nfrom discussing the bas
ic model\, I will also talk about some\ntechniques to tradeoff between its
expressiveness and analysis\ncomplexity.\n\nThis talk is based on joint w
ork with PS Thiagarajan from the National\nUniversity of Singapore\, and L
inh T.X. Phan and Insup Lee from the\nUniversity of Pennsylvania.\n\nBio:\
nSamarjit Chakraborty is a Professor of Electrical Engineering at the\nTec
hnical University of Munich\, where he heads the Institute for\nReal-Time
Computer Systems. He obtained his Ph.D. in Electrical and\nComputer Engine
ering from ETH Zurich in 2003. Prior to joining TU\nMunich\, from 2003 --
2008 he was an Assistant Professor of Computer\nScience at the National Un
iversity of Singapore. His research\ninterests are primarily in system-lev
el power/performance analysis of\nreal-time and embedded systems.
LOCATION:TUM Garching\, Room 03.09.014\n
CONTACT:Chakraborty Samarjit
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094AL0d@lapbroy149
DTSTART;TZID=Europe/Berlin:20131209T160000
DTEND;TZID=Europe/Berlin:20131209T170000
SUMMARY:Thiagarajan P.S.: Analysis of Continuous Dynamical Systems Via Stat
istical Model Checking
DESCRIPTION:Systems with real-valued variables that evolve continuously w.r
.t. time arise\nin many settings including cyber-physical systems and bioc
hemical networks.\nThe dynamics of these variables will be typically speci
fied in terms of differ-\nential equations. An important verification task
is to determine whether the\nglobal behavior of the system has the requir
ed reachability properties. The\nnumber of the the real-valued variables c
an be large and their dynamics can\nbe non-linear. Further\, there can be
multiple modes of behavior where each\nmode is governed by a different sys
tem of differential equations. Hence such\nsystems can seldom be analyzed
effectively let alone efficiently.\nWe advocate statistical model checking
as an approximate but scalable\nanalysis technique in these settings. The
basic idea is to assume a proba-\nbility distribution over the initial st
ates of the system. This in turn -under\nsuitable continuity assumptions-
induces a distribution over the trajectories\ngenerated by the initial sta
tes. Hence one can construct a statistical model\nchecking procedure to ve
rify interesting dynamical properties using a simple\nsequential hypothesi
s testing method. We demonstrate the applicability of\nthis approach using
a number of large biopathways models.
LOCATION:TUM Garching - 03.13.010
URL:http://www.model.in.tum.de/~frieling/2013-12-09-Thiagarajan-2_ode.pptx
CONTACT:Thiagarajan P.S.
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094As7h@lapbroy149
DTSTART;TZID=Europe/Berlin:20100708T101500
DTEND;TZID=Europe/Berlin:20100708T111500
SUMMARY:Mnich Matthias: Feedback Vertex Sets in Tournaments
DESCRIPTION:Abstract: For a tournament $T$\, a feedback vertex set is a sub
set of vertices intersecting every directed cycle of $T$. We prove that ev
ery tournament on $n$ vertices has at most $1.6740^n$ minimal feedback ver
tex sets and some tournaments have $1.5448^n$ minimal feedback vertex sets
. This improves an old result by Moon from 1971. Moreover\, we give the fi
rst polynomial-space polynomial-delay algorithm for enumerating all minima
l feedback vertex sets. As corollary we derive the fastest exponential-tim
e algorithm for finding a feedback vertex set of minimum size. (Joint work
with Serge Gaspers\, Universidad de Chile)
LOCATION:Room 02.04.011 at TUM Garching
CONTACT:Mnich Matthias
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094AT5Y@lapbroy149
DTSTART;TZID=Europe/Berlin:20100701T160000
DTEND;TZID=Europe/Berlin:20100701T170000
SUMMARY:Droste Manfred: Weighted automata and quantitative logics
DESCRIPTION:In automata theory\, a classical result of B\\uchi states that\
\nthe recognizable languages are precisely the ones definable by\\nsentenc
es of monadic second order logic. We will present a\\ngeneralization of th
is result to the context of weighted automata.\\nA weighted automaton is a
classical nondeterministic automaton\\nin which each transition carries a
weight describing e.g. the\\nresources used for its execution\\\, the len
gth of time needed\\\, or\\nits reliability. The behavior (language) of su
ch a weighted automaton\\nis a function associating to each word the weigh
t of its execution.\\nWe develop syntax and semantics of a quantitative lo
gic\\\;\\nthe semantics counts 'how often' a formula is true.\\n\\nOur mai
n results show that if the weights are taken either in\\nan arbitrary semi
ring or in an arbitrary bounded lattice\\\,\\nthen the behaviors of weight
ed automata are precisely the\\nfunctions definable by sentences of our qu
antitative logic.\\nThe methods also apply to recent quantitative automata
model\\nof Henzinger et al. where weights of paths are determined\\\, e.g
.\\\,\\nas the average of the weights of the path's transitions.\\nB\\\\uc
hi's result follows by considering the classical\nBoolean algebra {0\,1}.\
n\nJoint work with Paul Gastin (ENS Cachan)\, Heiko Vogler (TU Dresden)\,\
nresp. Ingmar Meinecke (Leipzig).\n
LOCATION:TUM Garching\, 02.07.014
URL:http://puma.in.tum.de/wiki/Puma_Talk_Manfred_Droste
CONTACT:Droste Manfred
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094AzOh@lapbroy149
DTSTART;TZID=Europe/Berlin:20130823T100000
DTEND;TZID=Europe/Berlin:20130823T110000
SUMMARY:Tankink Carst: Documentation and Formal Mathematics: Web Technology
meets Proof Assistants\n
DESCRIPTION:As the field of interactive theorem proving gains more high-imp
act projects\n(both in mathematics and computer science)\, it becomes a ne
cessity to document\nand disseminate the artefacts of formal proof\, in pa
rticular the proof scripts\nused as input to the proof assistant.\nIn this
talk\, I will describe several workflows for describing and publishing\nf
ormal proofs\, using modern web technologies. These workflows are implemen
ted in\na single prototype 'Wiki' platform\, that supports formalizations
in the Coq and\nHOL Light proof assistants\, and I will use the system to
demonstrate some of the\nworkflows.
LOCATION:Garching FMI 00.09.38
CONTACT:Tankink Carst
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094b2kk@lapbroy149
DTSTART;TZID=Europe/Berlin:20100818T160000
DTEND;TZID=Europe/Berlin:20100818T170000
SUMMARY:Dullien Thomas: Analysis of binaries
LOCATION:TUM Garching\, 02.07.014
CONTACT:Dullien Thomas
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094Bxyl@lapbroy149
DTSTART;TZID=Europe/Berlin:20090122T160000
DTEND;TZID=Europe/Berlin:20090122T170000
SUMMARY:Gast Holger: Approaches to Automated Reasoning about Heap-Manipulat
ing Programs
DESCRIPTION:Software verification in the large is feasible only with substa
ntial automation of proofs. Due to the details of aliasing\, pointer arith
metic\, and data structure invariants\, the challenge is specifically pron
ounced in the treatment of heap-manipulating programs.\n\nThe first part o
f the talk gives a high-level overview of fundamental approaches and their
recent contributions: separation logic yields concise specifications and
can be used for interactive functional verification\, while decidable frag
ments apply to the automatic verification of safety properties. Burstall's
split heap approach\, on the other hand\, supports record-based data stru
ctures and enables the application of existing automated reasoning techniq
ues.\n\nThe second part sketches the speaker's approach\, lightweight sepa
ration. It supports reasoning about memory layouts by specialized tactics\
, but uses classical HOL for assertions\, such that reasoning about them c
an rely on the automation already available in Isabelle.
LOCATION:Garching\, room MI 01.11.018
CONTACT:Gast Holger
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094c11t@lapbroy149
DTSTART;TZID=Europe/Berlin:20121130T100000
DTEND;TZID=Europe/Berlin:20121130T110000
SUMMARY:Tribastone Mirco: Continuous limits for massive-scale stochastic mo
dels of computing systems
DESCRIPTION:Fluid (or mean-field) techniques\, rooted in statistical mechan
ics and physical chemistry\, provide accurate deterministic approximations
to massive-scale Markov chain models of interacting agents. The original
discrete-state model is properly scaled in such a way that it converges to
the solution of a compact system of differential equations (ODEs) whose s
ize is independent from the population of agents.\n\nIn this seminar I wil
l overview recent results which relate the fluid approach and informatics
within the context of a stochastic process algebra\, as a means to dealing
with the infamous state-explosion problem of Markovian models of computin
g systems.\n\nThen\, I will introduce the concept of 'continuous-state exp
losion'\, which is exhibited by certain models that describe 'systems of s
ystems'\, for instance when a model comprises a large number of composite
processes and each consists of smaller processes which are themselves mass
ively replicated. In such conditions\, even fluid techniques are not scala
ble because the ODE system size grows polynomially with the population of
composite processes. Motivated by the fact that such a scenario is of prac
tical relevance (e.g.\, server farms and biological systems)\, I will disc
uss a novel notion of behavioural equivalence for ODEs that induces an exa
ct form of aggregation\, leading to a reduced ODE system which is complete
ly independent from all replicas.\n\nIf time permits\, I will then discuss
ongoing work which is pushing the limits of differential aggregations. I
will introduce a stochastic model that captures processes evolving spatial
ly over a discrete lattice. Whilst the analysis of such a model is computa
tionally infeasible even for coarse lattices\, I will present a form of ag
gregation that scales very well with the lattice size\, by capturing the i
nherently discrete movement in a continuous fashion via partial differenti
al equations of reaction-diffusion type.
LOCATION:Garching\, MI 02.07.014.
CONTACT:Tribastone Mirco
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094CdH@lapbroy149
DTSTART;TZID=Europe/Berlin:20111202T083000
DTEND;TZID=Europe/Berlin:20111202T093000
SUMMARY:Vytiniotis Dimitrios: Stop when you are Almost-Full Adventures in c
onstructive termination
DESCRIPTION:Disjunctive well-foundedness (used in Terminator)\, size-change
termination\, and well-quasi-orders (used in supercompilation and term-re
write systems) are examples of techniques that have been successfully appl
ied to automatic proofs of program termination and online termination test
ing\, respectively. Although these works originate in different communitie
s\, there is an intimate connection between them ? they rely on closely re
lated principles and both employ similar arguments from Ramsey theory. At
the same time there is a notable absence of these techniques in programmin
g sys- tems based on constructive type theory. In this paper we?d like to
highlight the aforementioned connection and make the core ideas widely acc
essible to theoreticians and Coq programmers\, by offer- ing a Coq develop
ment which culminates in some novel tools for performing induction. The be
nefit is nice composability properties of termination arguments at the cos
t of intuitive and lightweight user obligations. Inevitably\, we have to p
resent some Ramsey-like arguments: Though similar proofs are typically cla
ssical\, we offer an entirely constructive development standing on the sho
ulders of Veldman and Bezem\, and Richman and Stolzenberg.\n\nby Dimitrios
Vytiniotis\, MSR Cambridge
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Vytiniotis Dimitrios
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094CdnX@lapbroy149
DTSTART;TZID=Europe/Berlin:20100526T093000
DTEND;TZID=Europe/Berlin:20100526T103000
SUMMARY:Noschinski Lars: Automated Complexity Analysis of Term Rewrite Syst
ems
DESCRIPTION:Term Rewrite Systems are a simple calculus used for automated r
easoning and termination analysis of programs. For terminating rewrite sys
tems\, the runtime complexity is of particular interest. I present Complex
ity Dependency Tuples\, a modular framework for deriving feasible complexi
ty bounds for innermost TRS. CDTs are inspired by the successful Dependenc
y Pairs Framework for termination. They are designed to allow an easy adap
tion of existing techniques for this Framework.
LOCATION:TUM Garching\, 00.09.055
CONTACT:Noschinski Lars
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094cQZ1@lapbroy149
DTSTART;TZID=Europe/Berlin:20140122T150000
DTEND;TZID=Europe/Berlin:20140122T160000
SUMMARY:Dawar Anuj: On Tractable Approximations of Graph Isomorphism
DESCRIPTION:In this talk I will talk of families of equivalence relations t
hat\napproximate graph isomorphism and are polynomial-time decidable. The
\n Weisfeiler-Lehman method provides one such family which has a large\nva
riety of equivalent characterisations emerging separately from\nalgebra\,
combinatorics and logic\, which I will review. It is known\n(by Cai-Fuere
r-Immerman 1992) that no fixed level of the hierarchy\nexactly characteris
es isomorphism. This has recently inspired the\ndefinition of a new hiera
rchy of equivalences\, which I will present\,\nwhich can be seen as a stre
ngthening of the W-L method to algebras\nover finite fields.\n\nThis is jo
int work with Bjarki Holm.
LOCATION:TUM Garching - 03.011.018
URL:http://www.model.in.tum.de/~frieling/2014-01-22-Anuj-Dawar.pdf
CONTACT:Dawar Anuj
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094CTu9@lapbroy149
DTSTART;TZID=Europe/Berlin:20100113T143000
DTEND;TZID=Europe/Berlin:20100113T153000
SUMMARY:Dubslaff Clemens: Transition System Semantics of Message Sequence C
harts
DESCRIPTION:Message Sequence Charts (MSCs) provide an intuitive notation of
communication systems and are used in early steps of requirement specific
ation. The simplest form of MSCs considers only exchange of messages betwe
en several processes and its semantics is given by some partial order. Com
bining MSC scenarios can be conveniently done using MSC-graphs (MSGs). Sin
ce errors in early design steps have heavy impact to development costs and
reliability\, MSCs are popular subject of verification. Whereas model che
cking single MSCs is decidable\, it is well known that it is undecidable f
or asynchronous semantics of MSG. We will present a transition system repr
esentation of MSC (and MSG) where the traces are equal to partial order li
nearizations. These transition systems allow us to employ model checking r
esults for transition systems such as reachability analysis in well-struct
ured transition systems.
LOCATION:TUM Garching - 03.09.014
CONTACT:Dubslaff Clemens
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094cVip@lapbroy149
DTSTART;TZID=Europe/Berlin:20130821T140000
DTEND;TZID=Europe/Berlin:20130821T150000
SUMMARY:Kuehlwein Daniel: MaSh: Machine Learning for Sledgehammer
DESCRIPTION:Sledgehammer integrates automatic theorem provers in the proof
assistant\nIsabelle/HOL. A key component\, the relevance filter\, heuristi
cally ranks the\nthousands of facts available and selects a subset\, based
on syntactic similarity\nto the current goal. We introduce MaSh\, an alte
rnative that learns from\nsuccessful proofs. New challenges arose from our
zero-click vision: MaSh\nshould integrate seamlessly with the users' work
flow\, so that they benefit from\nmachine learning without having to insta
ll software\, set up servers\, or guide\nthe learning. The underlying mach
inery draws on recent research in the context\nof Mizar and HOL Light\, wi
th a number of enhancements. MaSh outperforms the old\nrelevance filter on
large formalizations\, and a particularly strong filter is\nobtained by c
ombining the two filters.\n(joint work with Jasmin Christian Blanchette\,
Cezary Kaliszyk and Josef Urban)\n\nDaniel studied mathematics in Tuebinge
n\, Birmingham and Bonn. He did his Diplom\non the Naproche project\, a na
tural language proof checker. For his PhD\, he's\ndeveloping machine learn
ing algorithms and tools for formal methods. Josef Urban\nand Daniel creat
ed MaLeS\, a learning based automatic tuning framework for\nautomated theo
rem provers. Together with Jasmin Blanchette\, Cezary Kaliszyk and\nJosef
Urban\, he is currently working on integrating learning into Isabelle.
LOCATION:Garching FMI 00.09.38
CONTACT:Kuehlwein Daniel
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094D8J@lapbroy149
DTSTART;TZID=Europe/Berlin:20100326T100000
DTEND;TZID=Europe/Berlin:20100326T110000
SUMMARY:King Andy: Automatic Abstraction for Congruences
DESCRIPTION:One approach to verifying bit-twiddling algorithms is to derive
Â \ninvariants between the bits that constitute the variables of a Â \npr
ogram. Such invariants can often be described with systems of Â \ncongruen
ces where in each equation $\\vec{c} \\cdot \\vec{x} = d \\mod m \n$\, (un
known variable m)$ is a power of two\, $\\vec{c}$ is a vector of Â \ninteg
er coefficients\, and $\\vec{x}$ is a vector of propositional Â \nvariable
s (bits). Because of the low-level nature of these Â \ninvariants and the
large number of bits that are involved\, it is Â \nimportant that the tran
sfer functions can be derived automatically. Â \nWe address this problem\,
showing how an analysis for bit-level Â \ncongruence relationships can be
decoupled into two parts: (1) a SAT- \nbased abstraction (compilation) st
ep which can be automated\, and (2) Â \nan interpretation step that requir
es no SAT-solving. We exploit Â \ntriangular matrix forms to derive transf
er functions efficiently\, Â \neven in the presence of large numbers of bi
ts. Finally we propose Â \nprogram transformations that improve the analys
is results.
LOCATION:TUM Garching\, 02.07.014
CONTACT:King Andy
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094d9yC@lapbroy149
DTSTART;TZID=Europe/Berlin:20100917T140000
DTEND;TZID=Europe/Berlin:20100917T150000
SUMMARY:Manuel Fahndrich: Microsoft Research-Vortrag zur automatischen Veri
fizierung von Software Contracts mit Microsoft Clousot
DESCRIPTION:Im Zuge immer komplexerer und umfangreicherer Softwareentwicklu
ngsprojekte wird es zunehmend wichtiger\, entwickelte Software von Anfang
an umfangreich und effektiv zu testen\, um ein qualitativ hochwertiges Pro
dukt herzustellen. Kunden erwarten Software mit einem grossen Funktionsumf
ang und Komponenten\, die optimal aufeinander abgestimmt sind und die dabe
i noch ein Hoechstmass an Sicherheit bietet.\nDie Foerderinitiative Micros
oft Student Partners und das Graduiertenkolleg PUMA veranstalten am 17. Se
ptember 2010 einen Vortrag zum Thema Software Contracts mit Microsoft Clou
sot\, einem kostenfreien Tool zur automatischen Verifizierung von Software
Contracts. Manuel Fahndrich von Microsoft Research aus Redmond stellt Mic
rosoft Clousot vor und bietet damit einen Einblick\, wie Entwickler ihre P
rogramme durch Software Contracts sicherer gestalten koennen. Der Research
-Vortrag an der Informatik-Fakultaet der Technischen Universitaet Muenchen
\, Boltzmannstrasse 3\, Hoersaal 2\, 14:00 Uhr steht fuer alle Interessier
ten offen. Auf Grund einer begrenzten Anzahl an Sitzplaetzen werden Teilne
hmer gebeten\, sich online auf http://de.amiando.com/mspclousout.html anzu
melden.
LOCATION:TUM Garching\, Hoersaal 2
CONTACT:Manuel Fahndrich
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094DDoZ@lapbroy149
DTSTART;TZID=Europe/Berlin:20120127T083000
DTEND;TZID=Europe/Berlin:20120127T093000
SUMMARY:Klaedtke Felix: Policy Monitoring with First-order Temporal Logic
DESCRIPTION:In security and compliance\, it is often necessary to ensure th
at\nagents and systems comply to complex policies. An example of such a\n
policy from financial reporting is the requirement that every\ntransaction
of a customer c\, who has within the last 30 days been\ninvolved in a sus
picious transaction\, must be reported as suspicious\nwithin 2 days. In t
his talk\, I will give an overview of our approach\nto automated complianc
e checking. In particular\, I will present our\nmonitoring algorithm for
checking properties specified in a fragment\nof metric first-order tempora
l logic. I will also report on case\nstudies\, conducted together with No
kia\, in security and compliance\nmonitoring and use these to evaluate bot
h the suitability of this\nfragment for expressing complex\, realistic pol
icies and the efficiency\nof our tool MONPOLY\, which implements our monit
oring algorithm.\n\nJoint work with David Basin\, Matus Harvan\, Samuel Mu
eller\, and\nEugen Zalinescu.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Klaedtke Felix
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094dEqU@lapbroy149
DTSTART;TZID=Europe/Berlin:20130419T100000
DTEND;TZID=Europe/Berlin:20130419T110000
SUMMARY:Esparza Javier: Parameterized Verification of Asynchronous Shared-M
emory Systems\n
DESCRIPTION:We characterize the complexity of the safety verification probl
em forparameterized systems consisting of a leader process and arbitrarily
manyanonymous and identical contributors. Processes communicate through a
shared\, bounded-value register. While each operation on the registeris at
omic\, there is no synchronization primitive to execute a sequenceof opera
tions atomically. The model is inspired by distributedalgorithms implement
ed on sensor networks.We analyze the complexity of the safety verification
problem whenprocesses are modeled by finite-state machines\, pushdown mac
hines\, andTuring machines. Our proofs use combinatorial characterizations
ofcomputations in the model\, and in case of pushdown-systems\, some nove
llanguage-theoretic constructions of independent interest.
LOCATION:LMU A020
URL:http://www.model.in.tum.de/~frieling/2013-04-Javier-Esparza.pdf
CONTACT:Esparza Javier
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094drXZ@lapbroy149
DTSTART;TZID=Europe/Berlin:20100317T140000
DTEND;TZID=Europe/Berlin:20100317T150000
SUMMARY:Appel Andrew: Program Logics for Foundational Static Analysis
LOCATION:LMU Oettingerstr. 67\, L109
CONTACT:Appel Andrew
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094dtp5@lapbroy149
DTSTART;TZID=Europe/Berlin:20120615T083000
DTEND;TZID=Europe/Berlin:20120615T093000
SUMMARY:Philipp Hoffmann: Strategy Iteration on the Graphics Card
DESCRIPTION:Compared to standard CPUs\, graphic processing units (GPUs) off
er much\nhigher raw computational power at a lower price and energy\nconsu
mption. But in order to take full advantage of the GPU\, the\ncomputationa
l problem has to be suited for parallelization using\nvector operations wh
ich makes GPUs particularly well-suited for\nproblems relying largely on l
inear algebra. General-purpose computing\non the GPU is therefore widely u
sed today in computational sciences\ne.g. for simulation of physical syste
ms.\n In this bachelor thesis the use of the GPU for solving fixed-point\n
equations by means of the heuristic of strategy (or: policy) iteration\nis
studied specifically for games related to verification problems\nlike sim
ple stochastic games\, mean-payoff games\, or parity games.\n Solving thes
e games means solving a system of equations. Often\nsolving this system di
rectly is not possible. Strategy iteraiton\nreduces the problem of solving
the original system to that of a\nsequence of simpler equation systems.
Here simpler means that these\nsystems can be considered to be linear w.r
.t. a suitable algebraic\nstructure thereby becoming amenable for GPU comp
uting.\n In this talk\, I will discuss my progress at implementing a GPU b
ased\nsolver for parity games including the difficulties encountered so\n
far.
LOCATION:Amalienstr. 73\, Room 101
CONTACT:Philipp Hoffmann
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094DyUV@lapbroy149
DTSTART;TZID=Europe/Berlin:20130517T100000
DTEND;TZID=Europe/Berlin:20130517T110000
SUMMARY:Pérez Juan Navarro: Separation Logic Modulo Theories
DESCRIPTION:The aim of this talk is to describe a number of recent developm
ents on the integration of Separation Logic\, a prominent logic for static
ally reasoning about the memory usage of computer programs\, and Satisfiab
ility Modulo Theories (SMT). By leveraging on the power of SMT solvers\, o
ur reasoning tools are able to simultaneously handle supported theory asse
rtions between data and pointer variables---including e.g. integer and rea
l arithmetic\, bit-vectors and arrays---and the shape of the data structur
es referenced by those pointers. The talk will include motivating examples
and encouraging experimental results obtained with Asterix\, an implement
ation of our entailment checking algorithm that relies on Z3 as the theor
y reasoning back-end. This is joint work with Andrey Rybalchenko.
LOCATION:LMU main building\, A020
URL:http://www.model.in.tum.de/~frieling/2013-05-17-Navarro_Perez.pdf
CONTACT:PÃ©rez\n Juan Navarro
LAST-MODIFIED:20140313T141255Z
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094ebIh@lapbroy149
DTSTART;TZID=Europe/Berlin:20091111T100000
DTEND;TZID=Europe/Berlin:20091111T110000
SUMMARY:Logozzo Francesco: Clousot
DESCRIPTION:tba.
LOCATION:tba.
CONTACT:Logozzo Francesco
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094eeSi@lapbroy149
DTSTART;TZID=Europe/Berlin:20110614T140000
DTEND;TZID=Europe/Berlin:20110614T150000
SUMMARY:King Andy: Existential Quantification as Incremental SAT
DESCRIPTION:I shall present an algorithm for existential quantifier elimina
tion using incremental SAT solving. This approach contrasts with existing
techniques in that it is based solely on manipulating the SAT instance rat
her than requiring any reengineering of the SAT solver or needing an auxil
iary data-structure such as a BDD. The algorithm combines model enumeratio
n with the generation of shortest prime implicants so as to converge onto
a quantifier-free formula presented in CNF.\n\nThis is joint work with Joe
rg Brauer and Jael Kriener.
LOCATION:TUM Garching\, Room 02.07.034
CONTACT:King Andy
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094eKwp@lapbroy149
DTSTART;TZID=Europe/Berlin:20111014T150000
DTEND;TZID=Europe/Berlin:20111014T160000
SUMMARY:Hoffmann Jan: Types with Potential: Polynomial Resource Bounds via
Automatic Amortized Analysis
DESCRIPTION:A primary feature of a computer program is its quantitative\npe
rformance characteristics: the amount of resources such as time\,\nmemory\
, and power the program needs to perform its task. Concrete\nresource bou
nds for specific hardware have many important applications\nin software de
velopment but their manual determination is tedious and\nerror-prone.\n\nT
his dissertation studies the problem of automatically determining\nconcret
e worst-case bounds on the quantitative resource consumption of\nfunctiona
l programs.\n\nTraditionally\, automatic resource analyses are based on re
currence\nrelations. The difficulty of both extracting and solving recurr
ence\nrelations has led to the development of type-based resource analyses
\nthat are compositional\, modular\, and formally verifiable. However\,\n
existing automatic analyses based on amortization or sized types can\nonly
compute bounds that are linear in the sizes of the arguments of a\nfuncti
on.\n\nThis work presents a novel type system that derives polynomial reso
urce\nbounds from first-order functional programs. As pioneered by Hofman
n\nand Jost for linear bounds\, it relies on the potential method of\namor
tized analysis. Types are annotated with multivariate resource\npolynomia
ls\, a rich class of functions that generalize non-negative\nlinear combin
ations of binomial coefficients. The main theorem states\nthat type deriv
ations establish resource bounds that are sound with\nrespect to the resou
rce-consumption of programs which is formalized by a\nbig-step operational
semantics.\n\nSimple local type rules allow for an efficient inference al
gorithm for\nthe type annotations which relies on linear constraint solvin
g only.\nThis gives rise to an analysis system that is fully automatic if
a\nmaximal degree of the bounding polynomials is given. The analysis is\n
generic in the resource of interest and can derive bounds on time and\nspa
ce usage. The bounds are naturally closed under composition and\neventual
ly summarized in closed\, easily understood formulas.\n\nThe practicabilit
y of this automatic amortized analysis is verified with\na publicly availa
ble implementation and a reproducible experimental\nevaluation. The exper
iments with a wide range of examples from\nfunctional programming show tha
t the inference of the bounds only takes\na couple of seconds in most case
s. The derived heap-space and\nevaluation-step bounds are compared with t
he measured worst-case\nbehavior of the programs. Most bounds are asympto
tically tight\, and the\nconstant factors are close or even identical to t
he optimal ones.\n\nFor the first time we are able to automatically and pr
ecisely analyze\nthe resource consumption of involved programs such as qui
ck sort for\nlists of lists\, longest common subsequence via dynamic progr
amming\, and\nmultiplication of a list of matrices with different\, fittin
g dimensions.
LOCATION:Room 151 (Oettingenstr. 67)
CONTACT:Hoffmann Jan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094Et9g@lapbroy149
DTSTART;TZID=Europe/Berlin:20090608T171500
DTEND;TZID=Europe/Berlin:20090608T181500
SUMMARY:Best Elke: Cyclic Structure and Separability of Persistent Petri Ne
ts
DESCRIPTION:We prove that the reachability graph of a persistent and bounde
d\nPetri net can be decomposed into basic cycles which are either\nParikh-
disjoint or Parikh-equivalent. Based on this result\, we also \nprove\nth
at a persistent\, bounded\, reversible and plain Petri net is \n(weakly a
nd\nstrongly) separable\, revealing a relationship between a marking and
\nthe\nmarking divided by ist least common multiple.
LOCATION:HS2
CONTACT:Best Elke
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094F7K6@lapbroy149
DTSTART;TZID=Europe/Berlin:20090617T160000
DTEND;TZID=Europe/Berlin:20090617T170000
SUMMARY:Maneth Sebastian: MSO Definable Tree Transductions
DESCRIPTION:One of the fundamental connections between logic and automata w
as\nestablished by Buechi in the 60's: Monadic Second-Order (MSO) logic ov
er\nstrings has precisely the same expressiveness as finite-state automata
.\nThus\, we can use the theory of finite automata to give new decidabilit
y\nresults for MSO logic!\nThis result was later generalized to trees: MSO
logic over two\nsuccessors (i.e.\, over trees) has the same expressivenes
s as\nfinite-state tree automata.\nIn the early 90's\, Courcelle and other
s found a way to use MSO logic\nfor the specification of translations\, ra
ther than for sets of objects\n(string\, trees\, or graphs). The key idea
is to use formulas with\none and two free variables in order to define the
nodes and edges\nof the output object\, respectively. The interpretation
of these formulas\non a given input object (graph) generates a translated
output\ngraph. If the input and output graphs are trees\, then the resulti
ng\nformalism specifies a tree translation.\nThe question arose whether th
ere exists an appropriate generalization\nof Buechi's result to tree trans
lations: is there a class of\nfinite-state tree transducers that has preci
sely the same\nexpressivness as the MSO definable tree translations?\nIn t
his talk we discuss the answer to this question\, and show\nthat particula
r tree transducers\, called macro tree transducers\,\nwhen restricted to l
inear size increase\, precisely characterize\nthe MSO definable tree trans
lations.\nWe also show important properties of MSO definable tree translat
ions\nand how they can be proved very shortly and elegantly. Through the\n
above equivalence to finite-state tree transducers\, such properties\nhave
helped to identify important new properties of tree transducers\n(which w
ere too difficult to reason about without the connection\nto MSO logic)\;
thus\, we point out the usefulness of MSO logic over\nfinite-state formali
sms\, in the context of tree translations.
LOCATION:TUM Garching - 02.07.034
CONTACT:Maneth Sebastian
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094fP4f@lapbroy149
DTSTART;TZID=Europe/Berlin:20120206T161500
DTEND;TZID=Europe/Berlin:20120206T171500
SUMMARY:Moser Georg: Predicative Recursion and Register Machines
DESCRIPTION:In this talk I will propose a termination order\, dedicated for
\ncomplexity analysis\, the small polynomial path order (sPOP* for short)
. \nThis order provides a new characterisation of the class of polytime \n
computable function via term rewrite systems. Based on sPOP*\, we'll \nstu
dy a class of rewrite systems\, dubbed systems of predicative \nrecursion
of degree d\, such that for rewrite systems in this class we \nobtain that
the runtime complexity lies in O(n^d). We show that \npredicative recursi
ve rewrite systems of degree d define functions \ncomputable on a register
machine in time O(n^d). This result emphasises \nthe fact that (innermost
) runtime complexity of a rewrite system is an \ninvariant cost model.
LOCATION:Oettingerstr.\, L109
CONTACT:Moser Georg
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094FT8G@lapbroy149
DTSTART;TZID=Europe/Berlin:20120119T083000
DTEND;TZID=Europe/Berlin:20120119T093000
SUMMARY:Barth Stephan: SAT-based minimization for nondeterministic Buechi a
utomata
DESCRIPTION:Buechi Automata are an automaton model for describing infinite
languages.\nDespite its similarities to finite automata determinisation is
not\nalways possible in this model and no canonical minimization algorith
m\nexists.\n\nThis work describes SAT-based minimization procedure for non
deterministic Buechi automata (NBA).\n\nFor a given NBA A the procedure fi
nds an equivalent NBA A_min\nwith the minimal number of states. This is do
ne by successively\ncomputing automata A' that approximate A in the sense
that they\naccept a given finite set of positive examples and reject a giv
en\nfinite set of negative examples. In the course of the procedure these\
nexample sets are successively increased. Thus\, our method can be seen\na
s an instance of a generic learning algorithm based on a\nminimally adequa
te teacher in the sense of Angluin.\n\nWe use a SAT solver to find NBA for
given sets of positive and\nnegative examples. We use Ramsey-based comple
mentation to check\ncandidates computed in this manner for equivalence wit
h A. Failure\nof equivalence yields new positive or negative examples. O
ur method\nproved successful on a series of small examples that are nontri
vial in\nthe sense that they are difficult or impossible to minimize by\nh
and. In particular\, we succeed in minimizing all NBA with two states\nand
two-letter alphabet as well as some instances of Michel's NBA\nwhich were
introduced to establish an n!\nlower bound on complementation of NBA.
LOCATION:LMU\, Oettingenstr 67\, L109
CONTACT:Barth Stephan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094fudG@lapbroy149
DTSTART;TZID=Europe/Berlin:20091030T100000
DTEND;TZID=Europe/Berlin:20091030T110000
SUMMARY:Hoare Tony: tba.
DESCRIPTION:tba.
LOCATION:tba.
CONTACT:Hoare Tony
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094FvMQ@lapbroy149
DTSTART;TZID=Europe/Berlin:20120216T170000
DTEND;TZID=Europe/Berlin:20120216T180000
SUMMARY:Broadbent Christian: Approaches to Model-Checking Higher-Order Recu
rsion Schemes: The Automata-Theoretic Perspective in Context
DESCRIPTION:Higher-order recursion schemes (HORS) can be viewed as simply t
yped terms in \nthe lambda-calculus with recursion and thereby provide a u
seful model for the \nbehaviour of higher-order functional programs. Since
Ong's original proof \n[LICS 2006] that the mu-calculus model-checking i
s decidable on structures \ngenerated by HORS\, a number of alternative al
gorithms have been developed. In \nparticular variants of Kobayashi's algo
rithm based on intersection types [POPL \n2009] have been implemented and
show promise as being usable in practise.\n\nAnother way of looking at the
problem is to consider a different but equivalent \nmodel to HORS---namel
y `collapsible pushdown automata' (CPDA) [Hague et al. \nLICS 2008]. A CPD
A has a memory consisting of a `pushdown of pushdowns.... of \npushdown st
acks' together with additional structure in the form of `links'. \nOne can
define a natural class of automata recognising sets of CPDA \nconfigurati
ons that provide a way to represent a solution to the global mu-\ncalculus
model-checking problem for CPDA (and hence HORS) [B. et al. LICS \n2010].
\n\nIn this talk we will introduce HORS and CPDA together with a brief ov
erview of \nthe techniques mentioned above. Our main focus will\, however\
, be on CPDA\; in \nparticular we will outline some very recent work in pr
ogress [joint with \nArnaud Carayol\, Matthew Hague\, Olivier Serre] to de
velop a saturation \nalgorithm for CPDA\, which we eventually hope to impl
ement to provide a point \nof comparison with the intersection type algori
thms that work directly on \nHORS. We will conclude by highlighting some p
ossible deep connections between \nthe intersection type and CPDA approach
es\, which suggest that further down the \nline the two techniques may be
able to inform each other.
LOCATION:TUM Garching - Room 03.09.014
CONTACT:Broadbent Christian
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094gBYw@lapbroy149
DTSTART;TZID=Europe/Berlin:20130524T103000
DTEND;TZID=Europe/Berlin:20130524T113000
SUMMARY:Bouajjani Ahmed: Verifying Concurrent Programs against Sequential S
pecifications.
DESCRIPTION:We investigate the algorithmic feasibility of checking whether
concurrent\nimplementations of shared-memory objects adhere to their given
sequential\nspecifications\; sequential consistency\, linearizability\, a
nd conflict\nserializability are the canonical variations of this problem.
While verifying\nsequential consistency of systems with unbounded concurr
ency is known to be\nundecidable\, we demonstrate that conflict serializab
ility\, and linearizability\nwith fixed linearization points are EXPSPACE-
complete\, while the general\nlinearizability problem is undecidable.\n\nO
ur (un)decidability proofs\, besides bestowing novel theoretical results\,
also\nreveal novel program explorations strategies. For instance\, we sho
w that every\nviolation to conflict serializability is captured by a confl
ict cycle whose\nlength is bounded independently from the number of concur
rent operations. This\nsuggests an incomplete detection algorithm which on
ly remembers a small subset\nof conflict edges\, which can be made complet
e by increasing the number of\nremembered edges to the cycle-length bound.
Similarly\, our undecidability proof\nfor linearizability suggests an inc
omplete detection algorithm which limits the\nnumber of ``barriers'' bisec
ting non-overlapping operations. Our decidability\nproof of bounded-barrie
r linearizability is interesting on its own\, as it\nreduces the considera
tion of all possible operation serializations to numerical\nconstraint sol
ving. The literature seems to confirm that most violations are\ndetectable
by considering very few conflict edges or barriers.\n\n(Joint work with C
onstantin Enea\, Michael Emmi\, and Jad Hamza. Published in ESOP'13.)
LOCATION:LMU Main Building\, A020
CONTACT:Bouajjani Ahmed
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094GCdO@lapbroy149
DTSTART;TZID=Europe/Berlin:20120113T083000
DTEND;TZID=Europe/Berlin:20120113T093000
SUMMARY:Senjak Christoph-Simon: Minimal from Classical Proofs
DESCRIPTION:While minimal and intuitionistic derivability implies classical
\nderivability\, the converse only holds for special cases. One such case\
nis Barr's theorem\, which states that this converse holds for geometric\n
implications derivable from geometric theories\, another is the full\nclas
sification by means of positiveness of connectives\, given by\nOrevkov (19
68) and Nadathur (2000). We have a look at the runtime of\nthe algorithms
that the proofs of these theorems yield. For one of\nGlivenko's classes of
such sequents\, we can give an algorithm of\nquadratic runtime\, provided
it is in long normal form and given in a\nslightly weaker version of clas
sical logic. This is of interest for\ncomputational uses of classical proo
fs.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Senjak Christoph-Simon
LAST-MODIFIED:20140313T142628Z
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094gcod@lapbroy149
DTSTART;TZID=Europe/Berlin:20110211T100000
DTEND;TZID=Europe/Berlin:20110211T110000
SUMMARY:Baier Christel: On Model Checking Techniques for Randomized Distrib
uted Systems
DESCRIPTION:The automata-based model checking approach for randomized\ndist
ributed systems relies on an operational interleaving\nsemantics of the sy
stem by means of a Markov decision process\nand a formalization of the des
ired event E by an\nomega-regular linear-time property\, e.g.\, an LTL for
mula.\nThe task is then to compute the greatest lower bound for the\nproba
bility for E that can be guaranteed even in worst-case\nscenarios. Such b
ounds can be computed by a combination of\npolynomially time-bounded graph
algorithm with methods for\nsolving linear programs. In the classical ap
proach\, the\nworst-case is determined when ranging over all schedulers\nt
hat decide which action to perform next. In particular\, all\npossible int
erleavings and resolutions of other nondeterministic\nchoices in the syste
m model are taken into account.\n\nAs in the nonprobabilistic case\, the c
ommutativity of\nindependent concurrent actions can be used to avoid redun
dancies\nin the system model and to increase the efficiency of the\nquanti
tative analysis. However\, there are certain phenomena that\nare specific
for the probabilistic case and require additional\nconditions for the redu
ced model to ensure that the worst-case\nprobabilities are preserved. Rela
ted to this observation is also\nthe fact that the worst-case analysis tha
t ranges over all\nschedulers is often too pessimistic and leads to extrem
e\nprobability values that can be achieved only by schedulers that\nare un
realistic for parallel systems. This motivates the switch\nto more realis
tic classes of schedulers that respect the fact\nthat the individual proce
sses only have partial information\nabout the global system states. Such
classes of\npartial-information schedulers yield more realistic worst-cas
e\nprobabilities\, but computationally they are much harder. A wide\nrang
e of verification problems turns out to be undecidable when\nthe goal is t
o check that certain probability bounds hold under\nall partial-informatio
n schedulers.
LOCATION:TUM Garching\, Room 03.09.014\n
CONTACT:Baier Christel
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094gEgx@lapbroy149
DTSTART;TZID=Europe/Berlin:20110729T103000
DTEND;TZID=Europe/Berlin:20110729T113000
SUMMARY:Malkis Alexander: A generic privacy policy language
DESCRIPTION:We present a declarative language with a formal semantics for s
pecifying both\nusers' privacy preferences and services' privacy policies.
Expressiveness and\napplicability are maximized by keeping the vocabulary
and semantics of service\nbehaviours abstract. A privacy-compliant data-h
andling protocol for a network\nof communicating principals is described.
LOCATION:TUM Garching - Room 03.09.014
CONTACT:Malkis Alexander
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094gsMF@lapbroy149
DTSTART;TZID=Europe/Berlin:20100708T150000
DTEND;TZID=Europe/Berlin:20100708T160000
SUMMARY:Falk Heiko: Compilation and Optimization for hard Real-Time Systems
DESCRIPTION:During the design of software for hard real-time systems\, the
worst-case execution time (WCET) of a program plays an important role. Onl
y if the WCET is known\, it can be guaranteed that the software of a real-
time system always terminates within given timing constraints.\n\nHowever\
, the current state of the art in designing software for hard real-time sy
stems is heavily unsafe. On the one hand\, the actual industrial design pr
actice relies on measurements or simulations so that no guarantees about t
he worst-case timing of a piece of software can be derived. On the other h
and\, current compilers usually optimize the average-case execution time (
ACET) of a program\, instead of the WCET. Again\, there is no way to deriv
e conclusions about a program's worst-case timing if the program is optimi
zed w.r.t. the ACET.\n\nThis talk presents a WCET-aware compiler for hard
real-time systems. By tightly coupling the compiler with a tool for static
WCET analysis\, it is possible for the very first time to integrate a for
mal WCET timing model into a compiler. This WCET timing model provides the
compiler with valuable data about the worst-case behavior of a program to
be compiled and optimized.\n\nThis timing model is then used by specializ
ed optimizations which achieve a fully automatic minimization of the WCET.
In this talk\, two WCET minimizing optimizations are presented which focu
s in particular on the memory hierarchy of embedded processors: register a
llocation and scratchpad memory allocation.\n
LOCATION:TUM Garching\, 02.07.014
CONTACT:Falk Heiko
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094HFQD@lapbroy149
DTSTART;TZID=Europe/Berlin:20121026T083000
DTEND;TZID=Europe/Berlin:20121026T093000
SUMMARY:Hofmann Martin: Tutorial on type and effect systems
LOCATION:Garching\, MI 02.07.014.
CONTACT:Hofmann Martin
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094HOPz@lapbroy149
DTSTART;TZID=Europe/Berlin:20121130T110000
DTEND;TZID=Europe/Berlin:20121130T120000
SUMMARY:Krcal Jan: Fixed-delay Events in Generalized Semi-Markov Processes
Revisited
DESCRIPTION:In the area of probabilistic verification and performance evalu
ation\, the behavior of\nreal-life systems such as queues\, assembly lines
or communication protocols are\nanalyzed using formal mathematical models
\, such as Generalized Semi-Markov\nProcesses (GSMP). We consider a previo
usly studied class of GSMP extended\nwith events that occur after a fixed
delay. Disproving several previous results\, we\nshow that such GSMP can e
xhibit a surprisingly unstable behavior in the long-run.\nThe instability
is caused by properties of the model not found in real-life. To avoid\nthi
s undesirable situation\, we also provide syntactical conditions upon whic
h a GSMP\nmodel has always a stable behavior.
LOCATION:Garching\, MI 02.07.014
CONTACT:Krcal Jan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094I1gZ@lapbroy149
DTSTART;TZID=Europe/Berlin:20130726T100000
DTEND;TZID=Europe/Berlin:20130726T110000
SUMMARY:Runkler Thomas: Machine Learning\, industrial applications at Sieme
ns\, and an application to program analysis
DESCRIPTION:This talk will start with a short overview on machine learning
methods\, from supervised through unsupervised to reinforcement learning.
It will then sketch some real-world applications of machine learning at S
iemens in the industrial and energy domains. Finally\, the talk will focu
s on an application of machine learning to program analysis: Support vecto
r machines are used to identify individual procedures (corresponding to in
dividual stack frames) in PowerPC source code.
LOCATION:LMU main building A020
URL:http://www.model.in.tum.de/~frieling/2013-07-26-Runkler.pdf
CONTACT:Runkler Thomas
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094I5lp@lapbroy149
DTSTART;TZID=Europe/Berlin:20130621T100000
DTEND;TZID=Europe/Berlin:20130621T110000
SUMMARY:Durand-Gasselin Antoine: From Monadic Second-Order Definable String
Transformations to Transducers\n
DESCRIPTION:Courcelle (1992) proposed the idea of using logic\, in particul
ar\nMonadic second-order logic (MSO)\, to define graph to graph\ntransform
ations. When restricting the input to a string\, one can\ndevise executabl
e machine models to define such\ntransformations. Engelfriet and Hoogeboom
(2001) studied two-way\nfinite state string-to-string transducers and sho
wed that their\nexpressiveness matches MSO-definable transformations (MSOT
).\n\nAlur and ?ernÃ½ (2011) presented streaming transducers â??one-way\nt
ransducers equipped with multiple registers that can store output\nstrings
â?? as an equi-expressive model. Natural generalizations of\nstreaming tra
nsducers to string-to-tree (Alur and Dâ??Antoni\, 2012) and\ninfinite-stri
ng-to-string (Alur\, Filiot\, and Trivedi\, 2012) cases\npreserve MSO-expr
essiveness.\n\nWhile earlier reductions from MSOT to streaming transducers
used two-way\ntransducers as the intermediate model\, I will revisit the
earlier\nreductions in a more general\, and previously unexplored setting
of\ninfinite-string-to-tree transformations\, and provide a direct\nreduct
ion. Proof techniques used for this new reduction exploit the\nconceptual
tools (composition theorem and finite additive coloring\ntheorem) presente
d by Shelah (1975) in his alternative proof of Buechiâ??s\ntheorem. Using
such streaming string-to-tree transducers yields\nnon-trivial decidability
results for instance the decidability of\nfunctional equivalence for MSO-
definable infinite-string-to-tree\ntransformations.\n(joint work with Raje
ev Alur and Ashutosh Trivedi\, to appear in LICS 2013)
LOCATION:LMU main building\, A020
URL:http://www.model.in.tum.de/~frieling/2013-06-21-Durand-Gasselin.pdf
CONTACT:Durand-Gasselin Antoine
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094i5ro@lapbroy149
DTSTART;TZID=Europe/Berlin:20110610T083000
DTEND;TZID=Europe/Berlin:20110610T093000
SUMMARY:Meyer Roland: Deciding robustness against total store ordering
DESCRIPTION:joint work with Ahmed Bouajjani (LIAFA) and Eike Moehlmann (Uni
versity of \nOldenburg)\n\nSequential consistency (SC) is the classical mo
del for shared memory\nconcurrent programs. It corresponds to the interlea
ving semantics where the \norder of actions issued by a component is prese
rved. For performance reasons\, \nmodern processors adopt relaxed memory m
odels that may execute actions out of \norder. We address the problem of d
eciding robustness of a program against the \ntotal store ordering (TSO) m
emory model\, i.e.\, we check whether the behaviour\nunder TSO coincides w
ith the expected SC semantics. We prove that this problem \nis PSPACE-comp
lete. The key insight is that violations to robustness can be \ndetected o
n pairs of SC computations.
LOCATION:LMU Main Building - A U117
CONTACT:Meyer Roland
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094i8ib@lapbroy149
DTSTART;TZID=Europe/Berlin:20130705T100000
DTEND;TZID=Europe/Berlin:20130705T110000
SUMMARY:Lammich Peter: Dynamic Pushdown Networks with Join and Contextual L
ocking
DESCRIPTION:Dynamic pushdown networks (DPNs) are a model for concurrent pro
grams\nwith procedures and thread-creation. In this talk\, we present an\n
extension of DPNs that support join-operations and contextual locking. A\n
join operation allows a thread to wait for the threads that it created\nto
terminate\, and contextual locking allows the acquisition and release\nof
locks\, where a procedure may only release locks that it acquired\, and\n
must release all locks before it returns.\n\nOur main results are that rea
chability is already PSPACE-complete for a\nconstant number of locks and 3
processes.\nFor dynamic thread creation without joining\, the problem rem
ains\nPSPACE-complete\, if we are only interested in reaching a configurat
ion\nwhere a constant-size subset of the processes is in certain states.\n
\nMoreover\, reachability of configurations described by a regular languag
e\nis still decidable\, even if we allow joining of processes.\n\njoint wo
rk with Markus Mueller-Olm\, Helmut Seidl\, and Alexander Wenner
LOCATION:LMU main building\, A020
URL:http://www.model.in.tum.de/~frieling/2013-07-05-Lammich.pdf
CONTACT:Lammich Peter
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094iY75@lapbroy149
DTSTART;TZID=Europe/Berlin:20130426T100000
DTEND;TZID=Europe/Berlin:20130426T110000
SUMMARY:Esparza Javier: On Negotiation as Concurrency Primitive\n
DESCRIPTION:We introduce negotiations\, a model of concurrency close to Pet
ri nets\, with multiparty negotiation as primitive. We study two problems:
soundness of negotiations (close to deadlock freedom)\, and the problem o
f\, given a negotiation with possibly many steps\,\ncomputing a summary\,
i.e.\, an equivalent one-step negotiation.\n\nWe provide a complete set of
reduction rules for acyclic\, weakly deterministic negotiations and show
that\, in the case of deterministic negotiations\, the rules compute the
summary in polynomial time.
LOCATION:LMU main building A020
CONTACT:Esparza Javier
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094J092@lapbroy149
DTSTART;TZID=Europe/Berlin:20090723T143000
DTEND;TZID=Europe/Berlin:20090723T153000
SUMMARY:Paulson Larry: An Automatic Theorem Prover for Real-Valued Special
Functions
DESCRIPTION:Logical formulas involving special functions such as ln\, exp a
nd sin can\nbe proved automatically by MetiTarski: a resolution theorem pr
over\nmodified to call a decision procedure for the theory of real closed\
nfields. (This theory in particular includes the real numbers with\nadditi
on\, subtraction and multiplication.) Special functions are\napproximated
by upper and lower bounds\, which are typically ratios of\npolynomials. Th
e decision procedure simplifies clauses by deleting\nliterals that are inc
onsistent with other algebraic facts\; the net\neffect is to split the pro
blem into numerous cases\, each covered by a\ndifferent approximation\, an
d to prove them individually. MetiTarski\nsimplifies arithmetic expression
s by conversion to a recursive\nrepresentation\, followed by flattening of
nested quotients. It can solve\nmany difficult problems found in mathemat
ics reference works\, and it can\nalso solve problems that arise from hybr
id and control systems.
LOCATION:TUM Garching - 03.09.14
CONTACT:Paulson Larry
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094J9j6@lapbroy149
DTSTART;TZID=Europe/Berlin:20120613T140000
DTEND;TZID=Europe/Berlin:20120613T150000
SUMMARY:Rafal Kolanski: Mechanised Separation Algebra for Isabelle/HOL
DESCRIPTION:I will be presenting our work on a Isabelle/HOL library with a
generic type class implementation of separation algebra based on the formu
lation by Calcagno et al. Our library features the basic separation logic
concepts developed on top of the separation algebra\, and contains automat
ed tactic support that can be used directly for any instantiation of the l
ibrary.\n
LOCATION:TUM Garching - Room 00.09.055
CONTACT:Rafal Kolanski
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094JfBN@lapbroy149
DTSTART;TZID=Europe/Berlin:20130503T100000
DTEND;TZID=Europe/Berlin:20130503T110000
SUMMARY:Cyriac Aiswarya: Model Checking Languages of Data Words
DESCRIPTION:We consider the model-checking problem for data multi- pushdown
automata (DMPA). DMPA generate data words\, i.e\, strings enriched with v
alues from an infinite domain. The latter can be used to represent an unbo
unded number of process identifiers so that DMPA are suitable to model con
current programs with dynamic process creation. To specify properties of d
ata words\, we use monadic second-order (MSO) logic\, which comes with a p
redicate to test two word positions for data equality. While satisfiabilit
y for MSO logic is undecidable (even for weaker fragments such as first-or
der logic)\, our main result states that one can decide if all words gener
ated by a DMPA satisfy a given formula from the full MSO logic.\n\nThis is
a joint work with Benedikt Bollig\, Paul Gastin and K. Narayan Kumar.\n\n
http://www.lsv.ens-cachan.fr/~cyriac/
LOCATION:LMU main building\, A020
URL:http://www.model.in.tum.de/~frieling/2013-05-03-Aiswarya_Cyriac.zip
CONTACT:Cyriac Aiswarya
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094JVik@lapbroy149
DTSTART;TZID=Europe/Berlin:20110715T083000
DTEND;TZID=Europe/Berlin:20110715T093000
SUMMARY:Klein Gerwin: Towards formally verifying security properties of mic
rokernel-based systems
DESCRIPTION:This talk presents our current work on the verification of secu
rity\nand safety properties on the code-level of embedded systems measurin
g\non the order of a million lines of code ore more. The key idea is to\nu
se the formally correct seL4 microkernel for reducing and analysing\nthe t
rusted computing base of such system. I will give an overview of\nthe curr
ent status of this work\, including an abstract security \nanalysis for a
case-study system\, and the proof that seL4 enforces the \nhigh-level secu
rity property 'integrity' down to the C code \nimplementation. I will sket
ch how this property helps us in \nreasoning about the behaviour of untrus
ted legacy system components.
LOCATION:LMU Main Building - A U117
CONTACT:Klein Gerwin
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094K2xi@lapbroy149
DTSTART;TZID=Europe/Berlin:20130328T100000
DTEND;TZID=Europe/Berlin:20130328T110000
SUMMARY:Marian Dan Andrei: Predicate Abstraction for Relaxed Memory Models
\n
DESCRIPTION:We present a novel approach for predicate abstraction of progra
ms running on relaxed memory models. Our approach consists of two steps. F
irst\, we reduce the problem of verifying a program P running on a memory
model M to the problem of verifying a program PM that captures an abstract
ion of M as part of the program. Second\, we show how to discover new pred
icates that enable verification of PM . The core idea is to extrapolate fr
om the predicates used to verify P under sequential consistency. A key new
concept is that of cube extrapolation: it successfully avoids exponential
state explosion when abstracting PM . We implemented our approach for the
x86 TSO and PSO memory models and showed that predicates discovered via e
xtrapolation are powerful enough to verify several challenging concurrent
programs. We show that our cube extrapolation method is enabling verificat
ion of additional programs. This is the first time some of these programs
have been verified for a model as relaxed as PSO.\n\nJoint work with Yuri
Meshman\, Martin Vechev and Eran Yahav.\n\nBio: Andrei Dan is a PhD studen
t at ETH Zurich where his adviser is Prof. Martin Vechev. Previously he ob
tained a M.Sc. degree from EPFL. His interests are in program analysis\, v
erification and concurrency.
LOCATION:Garching\, MI.02.07.014
URL:http://www.model.in.tum.de/~frieling/2013-03-Andrei-Dan.pdf
CONTACT:Marian Dan Andrei
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094kCpV@lapbroy149
DTSTART;TZID=Europe/Berlin:20101112T100000
DTEND;TZID=Europe/Berlin:20101112T110000
SUMMARY:Malacaria Pasquale: Quantifying Information Leaks in Software
DESCRIPTION:Abstract: Leakage of confidential information represents a seri
ous security risk. Despite a number of number of recent advances\, both th
eoretical and algorithmic\, it has been unclear if and how quantitative ap
proaches to measuring leakage of confidential information could be applied
to substantial\, real-world programs. This is mostly due to the high comp
lexity of computing precise leakage quantities. We introduce a technique w
hich makes it possible to decide if a program conforms to a quantitative p
olicy which scales to large state-spaces with the help of the bounded mode
l checker CBMC. Our technique is applied to a number of officially reporte
d information leak vulnerabilities in the Linux Kernel. Additionally\, we
also analysed authentication routines in the Secure Remote Password suite
and of a Internet Message Support Protocol implementation. Our technique s
hows when there is unacceptable leakage\; the same technique is also used
to verify\, for the first time\, that the applied software patches indeed
plug the information leaks. This is the first demonstration of quantitativ
e information flow addressing security concerns of real-world industrial p
rograms.
LOCATION:TUM Garching\, Room tba.
URL:http://puma.in.tum.de/wiki/Puma_talk_Pasquale_Malacaria
CONTACT:Malacaria Pasquale
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094kCYp@lapbroy149
DTSTART;TZID=Europe/Berlin:20101021T100000
DTEND;TZID=Europe/Berlin:20101021T110000
SUMMARY:Kennedy Andrew: F# and Units of Measure
LOCATION:LMU Institut fuer Informatik\, Oettingenstr. 67\, Muenchen\, L109
CONTACT:Kennedy Andrew
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094kD5u@lapbroy149
DTSTART;TZID=Europe/Berlin:20121212T103000
DTEND;TZID=Europe/Berlin:20121212T113000
SUMMARY:Brazil Tomas: Efficient Controller Synthesis for Consumption Games
with Multiple\nResource Types
DESCRIPTION:We introduce consumption games\, a model for discrete interacti
ve system with\nmultiple resources that are consumed or reloaded independe
ntly. More\nprecisely\,\na consumption game is a finite-state graph where
each transition is\nlabeled by a\nvector of resource updates\, where every
update is a non-positive number or\nomega. The omega updates model the re
loading of a given resource. Each\nvertex\nbelongs either to player Box or
player Diamond\, where the aim of player\nBox is\nto play so that the res
ources are never exhausted. We consider several\nnatural\nalgorithmic prob
lems about consumption games\, and show that although these\nproblems are
computationally hard in general\, they are solvable in\npolynomial\ntime f
or every fixed number of resource types (i.e.\, the dimension of\nthe upda
te\nvectors) and bounded resource updates.\n\nThis is a joint work with Kr
ishnendu Chatterjee\, Antonin Kucera and\nPetr Novotny.
LOCATION:Garching MI 02.07.014
CONTACT:Brazil Tomas
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094KGSV@lapbroy149
DTSTART;TZID=Europe/Berlin:20131115T100000
DTEND;TZID=Europe/Berlin:20131115T110000
SUMMARY:Althoff Matthias: Formal Verification of Cyber-Physical Systems\n
DESCRIPTION:Functionality\, autonomy\, and complexity of products and produ
ction\nprocesses is steadily increasing due to growing computing resources
. The\nadvanced capabilities of new systems make it possible to automate t
asks\nthat were previously performed by humans\, such as (semi-)automated\
noperation of road vehicles\, surgical robots\, smart grids\, flight contr
ol\nsystems\, and collaborative human-robot systems\, to name only a few.
It\nis obvious that most of those systems are either safety- or\noperation
-critical\, demanding methods that automatically verify their\nsafety and
correct operation.\n\nIn this talk\, I present reachability analysis as a
method to formally\nverify cyber-physical systems. I use hybrid automata t
o jointly model\nthe discrete behavior of computing elements and the conti
nuous behavior\nof the physical elements. Based on this modeling formalism
\, I present\nalgorithms for reachability analysis\, which automatically e
xplore all\npossible states of the system for a given set of initial state
s\,\nparameters\, and inputs. If the set of reachable states is not in a s
et\nof forbidden states\, the correct behavior of the system is proven. No
te\nthat this is not possible with classical simulation techniques\, since
\nthey only generate a finite and thus incomplete set of behaviors.\n\nThe
applicability of the method is demonstrated for autonomous driving\,\npha
se-locked loops\, and smart grids. In the remainder of the talk\,\nfuture
research directions for compositional verification\, model-based\ndesign t
echniques\, and fault-tolerant systems are suggested.
LOCATION:TUM Garching - 02.07.014
URL:http://www.model.in.tum.de/~frieling/2013-11-15-Matthias-Althoff.pdf
CONTACT:Althoff Matthias
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094ktYm@lapbroy149
DTSTART;TZID=Europe/Berlin:20111118T083000
DTEND;TZID=Europe/Berlin:20111118T093000
SUMMARY:Schwoon Stefan: Efficient contextual unfolding
DESCRIPTION:A contextual net is a Petri net extended with read arcs\, which
\nallow transitions to check for tokens without consuming them.\nContextua
l nets allow for better modelling of concurrent read\naccess than Petri ne
ts\, and their unfoldings can be\nexponentially more compact than those of
a corresponding Petri\nnet. A constructive but abstract procedure for gen
erating those\nunfoldings was proposed in earlier work\; however\, no conc
rete\nimplementation existed. Here\, we close this gap providing two\nconc
rete methods for computing contextual unfoldings\, with\na view to efficie
ncy. We report on experiments carried out on\na number of benchmarks. Thes
e show that not only are\ncontextual unfoldings more compact than Petri ne
t unfoldings\,\nbut they can be computed with the same or better efficienc
y\, in\nparticular with respect to the place-replication encoding of\ncont
extual nets into Petri nets.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Schwoon Stefan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094ljw7@lapbroy149
DTSTART;TZID=Europe/Berlin:20100611T083000
DTEND;TZID=Europe/Berlin:20100611T093000
SUMMARY:Rybalchenko Andrey: A proof rule for multi-threaded programs
DESCRIPTION:I will present a proof rule for the verification of temporal sa
fety and liveness properties of multi-threaded programs that facilitates m
odular reasoning when possible\, and provides for non-modular reasoning wh
en unavoidable. Then\, I will show how this rule can be transformed into a
n automatic method
LOCATION:LMU Main Building - A 011
CONTACT:Rybalchenko Andrey
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094ltbr@lapbroy149
DTSTART;TZID=Europe/Berlin:20100625T083000
DTEND;TZID=Europe/Berlin:20100625T093000
SUMMARY:Sewell Thomas: L4.verified: An Overview\, Partial Automation of Inv
ariant Proofs in Isabelle/HOL
DESCRIPTION:1) L4.verified: An Overview\n\nThe L4.verified project\, demons
trating the functional correctness of the\nseL4 microkernel\, was recently
completed by NICTA. This makes seL4 the\nworld's first verified general-p
urpose operating system kernel\, and\nmarks a significant step forward in
the application of formal methods to\nsystem software. In this talk I will
give an overview of the project\,\nincluding an introduction to the vario
us specifications of seL4's\nbehaviour used in the project and an outline
the methodology used in\nproving refinement between them. I will conclude
by discussing three\ndirections in which the verification is being extende
d\, and the evolving\ndirection in which we aim to put the verification in
to practical use.\n\n2) Partial Automation of Invariant Proofs in Isabelle
/HOL\n\nIn this talk I will focus on a single aspect of the L4.verified pr
oof\neffort: that of demonstrating that monadic models of the system respe
ct\ncertain invariants. While both invariant proofs and the Hoare Logic we
\nuse have been well studied\, a number of original challenges arise in ou
r\nspecific environment. These include handling of large databases of Hoar
e\nrules\, addressing recursive functions\, and managing the boundary betw
een\nuser-driven and interactive proof within the Isabelle/HOL proof\nenvi
ronment. I will conclude with some thoughts about how proof\nautomation mi
ght better serve such large projects in the future.
LOCATION:LMU Main Building - A 011
CONTACT:Sewell Thomas
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094m0n@lapbroy149
DTSTART;TZID=Europe/Berlin:20130118T100000
DTEND;TZID=Europe/Berlin:20130118T110000
SUMMARY:Hofmann Martin: Type-Based Enforcement of Secure Programming Guidel
ines Code Injection Prevention at SAP
DESCRIPTION:Code injection and cross-site scripting belong to the most comm
on security vulnerabilities in modern software\, usually caused by incorre
ct string processing. These exploits are often addressed by formu- lating
programming guidelines or â??best practicesâ?.\nIn this paper\, we study
the concrete example of a guideline used at SAP for the handling of untrus
ted\, potentially executable strings that are embedded in the output of a
Java servlet. To verify adherence to the guideline\, we present a type sys
tem for a Java-like language that is extended with refined string types\,
output effects\, and polymorphic method types.\nThe practical suitability
of the system is demonstrated by an imple- mentation of a corresponding st
ring type verifier and context-sensitive inference for real Java programs.
LOCATION:Garching MI 02.07.014
CONTACT:Hofmann Martin
LAST-MODIFIED:20140313T142541Z
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094M8Vv@lapbroy149
DTSTART;TZID=Europe/Berlin:20120801T143000
DTEND;TZID=Europe/Berlin:20120801T153000
SUMMARY:Giro Sergio: Verification of distributed probabilistic systems unde
r partial information\n
DESCRIPTION:Abstract:\n\nIn the verification of systems that involve probab
ilities\, it is\ncrucial to study qualitative properties concerning the pr
obability of\ncertain events as\, for instance\, the probability that a fa
ilure\\noccurs is less that 0.01. In case the system under consideration i
s\ndistributed\, each of the components of the system might have a partial
\nview of the information available to other components. The analysis of\n
these systems is carried out by considering distributed adversaries\nwith
restricted observations. In this talk I will summarise six years\nof resea
rch on automatic verification of distributed probabilistic\nsystems. On th
e negative side\, we proved the verification problem to\nbe undecidable in
general and NP-complete for some restricted systems.\nNevertheless\, we a
lso introduced some techniques for overestimation of\nworst-case probabili
ties\, and showed that the concept of distributed\nadversaries can be used
to improve existing techniques such as partial\norder reduction.
LOCATION:TUM Garching - Room 00.09.055
CONTACT:Giro Sergio
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094mmrr@lapbroy149
DTSTART;TZID=Europe/Berlin:20000101T000000
DTEND;TZID=Europe/Berlin:20000101T010000
SUMMARY:Ludwig Michael: Der Algorithmus von Howgrave-Graham und Joux zur Lo
esung schwerer Rucksackinstanzen
DESCRIPTION:Im Vortrag wird der aktuelle Algorithmus zur Loesung schwerer\n
Rucksackinstanzen von Howgrave-Graham und Joux aus dem Jahr 2009\nvorgeste
llt. Dies geschieht unter Zuhilfenahme der\nVorgaengeralgorithmen von Schr
oeppel und Shamir (1981) beziehungsweise\nHorowitz und Sahni (1974). Der a
ktuelle Algorithmus ist\, im Gegensatz\nzu den beiden Vorgaengern\, random
isiert und verwendet eine Heuristik.\nDer Fokus soll nicht auf der Korrekt
heit der Heuristik liegen\, sondern\nauf der Kernidee hinter dem neuen Ans
atz\, der sogenannten\nRepraesentationstechnik. Ausserdem liefert dieser A
lgorithmus einen\nTradeoff zwischen Speicher und Zeit. Im Vortrag wird gez
eigt\, wie\ndieser erweitert werden kann.
LOCATION:Amalienstr. 73a\,\nRaum 101.
CONTACT:Ludwig Michael
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094MtwE@lapbroy149
DTSTART;TZID=Europe/Berlin:20090506T141500
DTEND;TZID=Europe/Berlin:20090506T151500
SUMMARY:Sassone Vladimiro: Permission-based separation logic for message-pa
ssing concurrency
DESCRIPTION:The talk presents new local reasoning techniques for message\np
assing concurrent programs based on ideas from separation logics and\nreso
urce usage analyses. We propose a two-step analysis in which\nconcurrent
processes are first analysed for confluent behaviour using\na type and eff
ect system which provides a foundation for establishing\ncorrectness throu
gh logical\, separation-based reasoning.
LOCATION:Oettingenstrasse 67\, Raum Z1.09
CONTACT:Sassone Vladimiro
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094N1iT@lapbroy149
DTSTART;TZID=Europe/Berlin:20110204T100000
DTEND;TZID=Europe/Berlin:20110204T110000
SUMMARY:Beyer Dirk: Adjustable-Block Encoding: Towards a Unified Framework
for Software Verification
DESCRIPTION:Several successful software model checkers are based on a techn
ique called\nsingle-block encoding (SBE)\, which computes costly predicate
abstractions after\nevery single program operation. Large-block encoding
(LBE) computes\nabstractions only after a large number of operations\, an
d it was shown that\nthis significantly improved the verification performa
nce. In this work\, we\npresent adjustable-block encoding\, a unifying fr
amework that allows to express\nboth previous approaches. In addition\, i
t provides the flexibility to specify\nany block size between SBE and LBE\
, and also beyond LBE\, through the adjustment\nof several parameters. Su
ch a unification of different concepts makes it\neasier to understand the
fundamental properties of the analysis\, and makes the\ndifferences of the
variants more explicit. Adjustable-block encoding (ABE) is\nimplemented
as a configurable program analysis (CPA) in the verification\nframework CP
Achecker. We will also explain the architecture of that software\nand dem
onstrate how easy it is to plug-in new program analyses into this\nframewo
rk.
LOCATION:TUM Garching\, Room 03.09.014\n
URL:http://www.sosy-lab.org/
CONTACT:Beyer Dirk
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094NDco@lapbroy149
DTSTART;TZID=Europe/Berlin:20120627T160000
DTEND;TZID=Europe/Berlin:20120627T170000
SUMMARY:Koen Claessen: Automated first-order reasoning for Haskell program
verification
DESCRIPTION:We have recently developed various techniques for reasoning abo
ut\nHaskell programs which are all based on a translation from Haskell\npr
ograms to first-order logic and then using automated first-order\ntools to
reason about these. In this way\, we have built a contract\nchecker for H
askell programs\, an automated induction tool for Haskell\nprograms\, and
an automated counter example finder for Haskell\nprograms. I will discuss
successes and challenges\; all this is ongoing\nwork.\n\nThis is joint wor
k with the automated reasoning group at Chalmers:\nNick Smallbone\, Moa Jo
hansson\, Dan Rosen\, and myself\; and the Haskell\ngroup at Microsoft Res
earch: Dimitrios Vytiniotis and Simon\nPeyton-Jones.
LOCATION:TUM Garching - Room 00.09.055
CONTACT:Koen Claessen
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094NEuZ@lapbroy149
DTSTART;TZID=Europe/Berlin:20130208T100000
DTEND;TZID=Europe/Berlin:20130208T110000
SUMMARY:Terepeta Michal Tomasz: Recursive Advice for Coordination
DESCRIPTION:Aspect-oriented programming is a programming paradigm that is o
ften praised for the ability to create modular software and separate cross
-cutting concerns. Recently aspects have been also considered in thecontex
t of coordination languages\, offering similar advantages. However\, intro
ducing aspects makes analyzing such languages more difficult due to the fa
ct that aspects can be recursive â?? advice from an aspect must itself be
analyzed by aspects â?? as well as being simultaneously applicable in conc
urrent threads. Therefore the problem of reachability of various states of
a system becomes much more challenging. This is important since ensuring
that a system does not contain errors is often equivalent to proving that
some states are not reachable.\nIn this paper we show how to solve these c
hallenges by applying a successful technique from the area of software mod
el checking\, namely communicating pushdown systems. Even though primarily
used for analysis of recursive programs\, we are able to adapt them to fi
t this new context.
LOCATION:Garching MI 02.07.014
URL:http://www.model.in.tum.de/~frieling/2013-02-Michal-Terepeta.pdf
CONTACT:Terepeta Michal Tomasz
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094nq6K@lapbroy149
DTSTART;TZID=Europe/Berlin:20131209T100000
DTEND;TZID=Europe/Berlin:20131209T110000
SUMMARY:Thiagarajan P.S.: Approximate Verification of the Symbolic Dynamics
of Markov Chains
DESCRIPTION:We view a Markov chain as a linear transform operating over pro
bability\ndistributions over the states of the Markov chain. The iterative
applications\nof the chain M (i.e. its transition matrix) to an initial d
istribution over\nthe states will generate the trajectory. Thus a set of i
nitial distributions will\ninduce a set of trajectories. It is an interest
ing and useful task to analyze the\ndynamics of M as defined by this set o
f trajectories.\nThe novel idea here is to carry out this task in a symbol
ic framework.\nSpecifically\, we discretize the probability value space [0
\, 1] into a finite set of intervals I. A concrete probability distributio
n mu over the node of M is then symbolically represented as a tuple of int
ervals drawn from I where the i-th component of the tuple will be the inte
rval in which mu(i) falls. The set of these discretized distributions is a
finite alphabet.\nHence each trajectory will induce an infinite string ov
er this alphabet. Given\na set of initial distributions\, the symbolic dyn
amics of M will then consist of\nan infinite language L.\nThe goal is to v
erify whether L meets a specification given as a linear time\ntemporal log
ic formula. In our logic an atomic proposition will assert that\nthe curre
nt probability of a node falls in the interval I. Assuming\nL can be compu
ted effectively\, one can hope to solve our model checking\nproblem using
standard techniques in case L is an omega-regular\nlanguage. However we sh
ow that this is not always the case. Consequently\,\nwe develop the notion
of an epsilon-approximation\, based on the transient and long term behavi
ors of M . Briefly\, a symbolic trajectory is an epsilon-approximation of
another one iff (1) they agree during their transient phases\;\nand (2) bo
th trajectories are within an epsilon-neighborhood at all times after the
transient phase. Our main (related) results are that one can effectively c
heck whether (i) for each infinite word in L\, at least one of its epsilon
-approximations satisfies the given specification\; (ii) for each infinite
word in L\, all its epsilon-approximations satisfy the specification. The
se verification results are strong in that they apply to all finite state
Markov chains.
LOCATION:TUM Garching - 00.12.019
URL:http://www.model.in.tum.de/~frieling/2013-12-09-Thiagarajan-1_symbolic-
mc.pptx
CONTACT:Thiagarajan P.S.
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094nRuC@lapbroy149
DTSTART;TZID=Europe/Berlin:20120203T083000
DTEND;TZID=Europe/Berlin:20120203T093000
SUMMARY:Zeller Andreas: Experimental Program Analysis\, and how to get an E
RC grant
DESCRIPTION:In the past decade\, static validation of software systems has
made spectacular\nprogresses. However\, these techniques face enormous is
sues with the advent of\nmulti-site\, multi-language\, multi-vendor progra
ms such as Web applications\,\nwhich come with no specifications to rely o
n. In this talk\, I present an\nexperimental approach to software analysi
s\, where we generate executions to\nsystematically explore the space of s
oftware behavior ? and we use the outcome\nof these executions to guide th
e search even further. In contrast to static\ntechniques\, experimental t
echniques are applicable to arbitrary executable\nprograms\; in contrast t
o dynamic techniques\, they are not limited to just the\nobserved runs. E
ventually\, experimental techniques will provide precise\nspecifications t
o allow for large-scale formal verification.\n\nAndreas Zeller is a full p
rofessor for Software Engineering at Saarland\nUniversity in Saarbruecken\
, Germany. His research concerns the analysis of large\nsoftware systems a
nd their development process\; his students are funded by\ncompanies like
Google\, Microsoft\, or SAP. In 2010\, Zeller was inducted as\nFellow of t
he ACM for his contributions to automated debugging and mining\nsoftware a
rchives. In 2011\, he received an ERC Advanced Grant for work on\nspecific
ation mining and test case generation ? the topics of the above talk.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Zeller Andreas
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094NVY1@lapbroy149
DTSTART;TZID=Europe/Berlin:20120210T083000
DTEND;TZID=Europe/Berlin:20120210T093000
SUMMARY:Rossberg Andreas: Non-parametric Parametricity
DESCRIPTION:Type abstraction and intensional type analysis are features see
mingly at\nodds -- type abstraction is intended to guarantee parametricity
and\nrepresentation independence\, while type analysis is inherently\nnon
-parametric. A way to reconcile these features is to generate a fresh\ntyp
e name at run time when one defines an abstract type. That type\nname may
safely be used as a dynamic representative of the abstract type for\npurpo
ses of type analysis.\n\nBut does dynamic type generation provide us with
the same kinds of\nabstraction guarantees that we get from parametric poly
morphism? To give an\nanswer to that question\, we definene a step-indexed
Kripke logical\nrelation for a language with both non-parametric polymorp
hism (in the form\nof type-safe cast) and dynamic type generation. Our log
ical relation enables\nus to establish parametricity and representation in
dependence results\, even\nin a non-parametric setting\, by attaching arbi
trary relational\ninterpretations to dynamically-generated type names.\n\n
In addition\, we explore how programs that are provably equivalent in a mo
re\ntraditional parametric logical relation may be wrapped\;\nsystematical
ly to produce terms that are related by our non-parametric\nrelation\, and
vice versa. This leads us to develop a polarized\;\nvariant of our logica
l relation\, which enables us to distinguish formally\nbetween positive an
d negative notions of parametricity.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Rossberg Andreas
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094oGCw@lapbroy149
DTSTART;TZID=Europe/Berlin:20090826T160000
DTEND;TZID=Europe/Berlin:20090826T170000
SUMMARY:Hack Sebastian: Register Allocation for Programs in SSA Form
DESCRIPTION:Register allocation is one of the most important optimizations
in a modern\ncompiler. It maps the variables of a program to the processor
's registers in\norder to accelerate the program's execution.\n\nGraph col
oring\, as introduced by Chaitin\, has been the most popular and most\nsuc
cessful register allocation technique since its introduction in the late\n
1970s. It reduces the assignment problem to coloring the so-called\ninterf
erence graph that is constructed from the program to compile. Since\ngraph
coloring is NP-complete and each undirected graph can occur as an\ninterf
erence graph\, register allocation is NP-complete\, too.\n\nHowever\, if w
e require the program to be in static single-assignment form\n(SSA)\, a wi
dely used program representation\, interference graphs are no longer\ngene
ral. As we will show\, they belong to the class of chordal graphs. Their\n
most appealing property is that they can be colored optimally in quadratic
\ntime.\n\nWe present the theoretical properties of the interference graph
s of SSA\nprograms\, outline the differences to non-SSA programs\, and sho
w how the\nproperties of chordal graphs help to overcome the deficiencies
of traditional\nregister allocators.
LOCATION:TUM Garching - 02.07.014
CONTACT:Hack Sebastian
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094OiRp@lapbroy149
DTSTART;TZID=Europe/Berlin:20080412T160000
DTEND;TZID=Europe/Berlin:20080412T170000
SUMMARY:Kammueller Florian: ASPfun: Ein Kalkuel fuer Verteilte Aktive Objek
te in Isabelle/HOL
DESCRIPTION:Im Zeitalter des Internet muss sich das verteilte Rechnen mit a
synchronen parallelen Aktivitaeten\, Codeverteilung und komplexen Aufrufst
rukturen auseinandersetzen. Wir stellen in diesem Vortrag den Kalkuel ASPf
un fuer funktionale\, aktive Objekte vor. ASPfun erweitert die Theorie der
Objekte um eine Kommunikation mit einem Request-Reply-Mechanismus\, basie
rend auf sogenannten Futures. Futures repraesentieren erwartete Antworten
von Requests\; Replies geben das Ergebnis eines Requests an das Objekt zur
ueck\, das die entsprechende Future enthaelt.\n\nDieser Vortrag stellt zue
rst den ASPfun-Kalkuel und seine Semantik vor. Danach praesentieren wir ei
n Typsystem fuer ASPfun\, das Progress - und damit Verklemmungsfreiheit -
sicherstellt. ASPfun und seine Eigenschaften sind formalisiert und bewiese
n mit dem Theorembeweiser Isabelle.\n\n
CONTACT:Kammueller Florian
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094OmP1@lapbroy149
DTSTART;TZID=Europe/Berlin:20110819T083000
DTEND;TZID=Europe/Berlin:20110819T093000
SUMMARY:Talcott Carolyn: Pathway Logic: A Symbolic Systems Biology Framewor
k for Modeling Biological Processes
DESCRIPTION:Symbolic systems biology (SSB) is an approach to computational
modeling of biological\nsystems that builds on logical representations and
uses the symbolic reasoning tools\ndeveloped for analysis of complex hard
ware and software systems. Pathway Logic is an\napproach to SSB based on R
ewriting Logic\, a simple formalism for describing concurrent\nprocesses\,
such as cellular signaling. Process steps/reactions and related informati
on\nare collected as a network of in a knowledge base. Subnets and pathway
s are assembled\nas answers to queries (specifying desired outcomes or sit
uations to avoid) rather than\nbeing pre-defined. The Pathway Logic Assist
ant provides a graphical interface for\nbrowsing and analyzing such networ
ks.\n\nIn this talk we will explain the basics of Pathway Logic and give a
n overview of our\ncurated knowledge base of mamalian signaling reactions\
, including response to Egf\, Il1\,\nTnf-alpha. Then we will illustrate th
e use of the Pathway Logic Assistant to browse the\nreaction network\, and
find and compare pathways satisfying different constraints.
LOCATION:TUM Garching - Room 03.09.014
CONTACT:Talcott Carolyn
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094oTZm@lapbroy149
DTSTART;TZID=Europe/Berlin:20121123T100000
DTEND;TZID=Europe/Berlin:20121123T110000
SUMMARY:Hofmann Martin: Tutorial on type and effect systems
LOCATION:Garching\, MI 02.07.014
CONTACT:Hofmann Martin
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094pf0a@lapbroy149
DTSTART;TZID=Europe/Berlin:20131210T160000
DTEND;TZID=Europe/Berlin:20131210T170000
SUMMARY:Thiagarajan P.S.: Distributed Markov CHains
DESCRIPTION:TBA
LOCATION:TUM Garching - 02.13.010
URL:http://www.model.in.tum.de/~frieling/2013-12-10-Thiagarajan-3_dmc.pptx
CONTACT:Thiagarajan P.S.
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094PHMY@lapbroy149
DTSTART;TZID=Europe/Berlin:20101210T100000
DTEND;TZID=Europe/Berlin:20101210T110000
SUMMARY:Blanchet Bruno: Automatically Verified Mechanized Proof of One-Encr
yption Key Exchange
DESCRIPTION:We report on a case study of One-Encryption Key Exchange (OEKE)
\, a variant of\nthe Encrypted Key Exchange (EKE) protocol\, using CryptoV
erif. This work\nessentially consists in redoing the manual proof done by
Bresson et al\n(CCS'03)\, with the help of the automatic\, computationally
sound prover\nCryptoVerif\, which provides additional confidence that the
proof is correct.\nThis case study is an opportunity for important extens
ions of CryptoVerif\,\nwhich we will present. These extensions include sup
port for the computational\nDiffie-Hellman assumption and for proofs that
rely on Shoup's lemma. They also\ninclude additional game transformations
that insert case distinctions manually\nor merge cases that no longer need
to be distinguished. Eventually\, the\ncomputation of the probability bou
nds for attacks has also been improved\,\nproviding better reductions.\n\n
(joint work with David Pointcheval)
LOCATION:TUM Garching\, Room 03.09.014\n
CONTACT:Blanchet Bruno
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094PKXa@lapbroy149
DTSTART;TZID=Europe/Berlin:20110926T140000
DTEND;TZID=Europe/Berlin:20110926T150000
SUMMARY:Ka I Pun Violet: Polymorphic behavioural lock effects for deadlock
checking
DESCRIPTION:Deadlocks are a common problem for concurrent programs\, in par
ticular where\nmultiple threads are accessing shared mutually exclusive re
sources synchronized\nby locks. We use a behavioural type and effect syst
em to statically determine\npotential interaction of each thread with lock
s. Based on that thread-local\nlock interaction\, we explore the state sp
ace on the global level to detect\npotential deadlocks. In the presence o
f recursion\, we use two sound\nabstractions to keep the state space finit
e\, namely restricting the upper bound\nof re-entrant lock counters\, and
abstracting the behavioural effect into a\ncoarser\, tail recursive descri
ption.
LOCATION:TUM Garching - Room 03.09.014
CONTACT:Ka I Pun Violet
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094ppMu@lapbroy149
DTSTART;TZID=Europe/Berlin:20120125T170000
DTEND;TZID=Europe/Berlin:20120125T180000
SUMMARY:Maneth Sebastian: Fast In-Memory XPath Search using Compressed Inde
xes
DESCRIPTION:A large fraction of an XML document typically\nconsists of text
data. The XPath query language allows to\nsearch such text via its equal\
, contains\, and starts-with predicates\nThese predicates can be efficient
ly implemented using\na compressed self-index of the document's text data.
Most\nqueries\, however\, are hybrid: they contain parts which query\nthe
text of the document\, and contain other parts which query\nthe tree stru
cture of the document. It is therefore a challenge\nto appropriately choos
e a query evaluation order which optimally\nleverages the execution speeds
of the text and tree indexes.\nHere the SXSI system is introduced. It sto
res the tree\nstructure of an XML document using a bit array of opening\na
nd closing brackets plus a sequence of labels\, and stores\nthe text nodes
of the document using a global compressed\nself-index. On top of these in
dexes sits an XPath query en-\ngine that is based on tree automata. The en
gine uses fast\ncounting queries on the text index in order to determine\n
whether to evaluate top-down or bottom-up with respect to\nthe tree struct
ure. The resulting system has several advantages\nover existing systems: (
1) on pure tree queries (without\ntext search) such as the XPathMark queri
es\, the SXSI\nsystem performs on par or better than the fastest known sys
tems\nMonetDB and Qizx\, and (2) on queries that use text\nsearch\, SXSI o
utperforms the existing systems by 1-3 orders\nders of magnitude (dependin
g on the size of the result set)\,\nand (3) for all tested data and querie
s\, SXSI's memory consumption\nconsistently stays below two times the docu
ment size.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Maneth Sebastian
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094PVFq@lapbroy149
DTSTART;TZID=Europe/Berlin:20101217T101500
DTEND;TZID=Europe/Berlin:20101217T111500
SUMMARY:I-6 application talk
DESCRIPTION:Simon Barner (Easykit - model driven development for embedded s
oftware)\nMarkus Rickert (the Robotics library - open source software in r
obotics)\nSuraj Nair (OpenTL - a general purpose tracking library)\n[Optio
nal] Sarah Diot-Girard (Festo MPS systems - examples and programming langu
age)\n\nDuring the talk\, each presenter will first give a general stateme
nt on his/her work\, followed by showing you a small segment of the code a
nd explain its use.
LOCATION:TUM Garching\, Room 03.09.014\n
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094Px4@lapbroy149
DTSTART;TZID=Europe/Berlin:20130313T140000
DTEND;TZID=Europe/Berlin:20130313T150000
SUMMARY:Terauchi Tachio: A Template-based Approach to Complete Predicate Re
finement
DESCRIPTION:Predicate abstraction has proven successful for the verificatio
n of\nsoftware programs\, especially when it is combined with a\ncounterex
ample-guided predicate refinement (i.e.\, predicate inference)\nmethod. H
owever\, except for a few restricted first-order theories\,\nthe current p
redicate refinement methods are incomplete in that\nthe counterexample-gui
ded abstract-and-refine loop may fail to\nconverge even when an abstractio
n that is sufficient for verifying the\nprogram exists in the theory. Pre
dicate refinement is said to be\ncomplete when it is guaranteed to eventua
lly discover a sufficient\nabstraction\, when one exists in the underlying
first-order theory.\n\nThis talk presents a predicate refinement approach
that is\ncomplete for the quantifier-free theory of linear real arithmeti
c\nwith uninterpreted functions and arrays\, extending the previous\nstate
of the art on complete predicate refinement which was only\ncomplete for
more limited theories. Our approach is\ntemplate-based\, inspired by the
work on template-based (or\,\n``constraint-based'') program verification.
To make the approach\nscale\, we make an important observation that the f
irst-order\nlogic constraints that are solved to infer the predicates are\
nalways repetitions of certain patterns (they are generated from a\nset of
``Horn-clause like'' rules)\, so as to limit the expensive\ntemplate-base
d inference to a small number predicate variables in\nthe constraints.\n\n
This is a joint work with Hiroshi Unno and Naoki Kobayashi.
LOCATION:Garching MI 02.07.014
URL:http://www.model.in.tum.de/~frieling/2013-03-Tachio-Terauchi.pptx
CONTACT:Terauchi\n\n Tachio
LAST-MODIFIED:20140313T142442Z
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094quaw@lapbroy149
DTSTART;TZID=Europe/Berlin:20091223T090000
DTEND;TZID=Europe/Berlin:20091223T100000
SUMMARY:Gupta Ashutosh: From tests to proofs
DESCRIPTION:We describe the design and implementation of an automatic\ninva
riant generator for imperative programs. While automatic\ninvariant genera
tion through constraint solving has been\nextensively studied from a theor
etical viewpoint as a classical\nmeans of program verification\, in practi
ce existing tools do not\nscale even to moderately sized programs. This is
because the\nconstraints that need to be solved even for small programs a
re\nalready too difficult for the underlying (non-linear) constraint\nsolv
ing engines. To overcome this obstacle\, we propose to\nstrengthen static
constraint generation with information obtained\nfrom static abstract inte
rpretation and dynamic execution of the\nprogram. The strengthening comes
in the form of additional linear\nconstraints that trigger a series of sim
plifications in the solver\,\nand make solving more scalable. We demonstra
te the practical\napplicability of the approach by an experimental evaluat
ion on\na collection of challenging benchmark programs and comparisons\nwi
th related tools based on abstract interpretation and software\nmodel chec
king.\n
LOCATION:seminar room 02.07.014
CONTACT:Gupta Ashutosh
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094R3tu@lapbroy149
DTSTART;TZID=Europe/Berlin:20111013T140000
DTEND;TZID=Europe/Berlin:20111013T150000
SUMMARY:Ledesma-Garza Ruslan: Simplification of Horn clauses over unknown p
redicates
DESCRIPTION:The temporal verification of functional programs can be reduced
\nto constraint solving. The combination of our work on instrumenting\nfu
nctional programs and the Liquid Types inference system is a\ntechnique fo
r the verification of temporal properties of higher-order\nprograms. The
efficient solving of the subtyping constraints\ngenerated during type infe
rence is an important problem. There are\ncommon program features that ori
ginate subtyping constraints with\nredundant information. In this talk we
present a simplification rule\nover sets of subtyping constraints. Subtypi
ng constraints are\ninterpreted as Horn clauses over unknown predicates. W
e state our\nrule as a simplification rule over sets of Horn clauses that
preserves\nsatisfiability.
LOCATION:Fakultaet fuer Informatik Garching\, room 03.09.014
CONTACT:Ledesma-Garza Ruslan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094reoy@lapbroy149
DTSTART;TZID=Europe/Berlin:20101203T100000
DTEND;TZID=Europe/Berlin:20101203T110000
SUMMARY:Majumdar Rupak: Model Checking using Bounded Languages
DESCRIPTION:Abstract:\n\nBounded languages\, introduced by Ginsburg and Spa
nier\, are subsets of regular\nlanguages of the form w1*w2*... wk* for som
e words w1\,...\,wk. Bounded languages\nhave nice structural and decidabil
ity properties.\n\nWe show two applications of bounded languages in model
checking: first\, to\nunderapproximate the reachable state space of multit
hreaded procedural programs\nand second\, to underapproximate the reachabl
e state space of counter machines.\nIn particular\, we show that verificat
ion with bounded languages generalizes\ncontext-bounded reachability for m
ultithreaded programs.\n\nWe also show a new and constructive proof of the
following language-theoretic\nresult: for every context-free language L\,
there is a bounded context-free\nlanguage L' which is a subset of L and h
as the same Parikh image as L. \n\n(Joint work with Pierre Ganty and Benj
amin Monmege
LOCATION:TUM Garching\, Room 03.09.014\n
CONTACT:Majumdar Rupak
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094RMYb@lapbroy149
DTSTART;TZID=Europe/Berlin:20130712T100000
DTEND;TZID=Europe/Berlin:20130712T110000
SUMMARY:Broadbent Christopher: CSHORe and HorsSat(T): Saturation based hig
her-order model checking in practice.\n
DESCRIPTION:Higher-order recursion schemes (HORS) are a kind of grammar who
se non-terminals\nare simply typed. They provide a precise model of contro
l-flow in programs featuring\nhigher-order recursive functions. The model-
checking of HORS has various applications\nincluding the flow analysis and
verification of safety properties of such programs.\n\nCollapsible Pushdo
wn Systems (CPDS) are a generalisation of pushdown systems\nwith a nested
stack structure. CPDS are equi-expressive with HORS. In ICALP 2012\nwe pre
sented a `saturation algorithm' for checking safety properties of CPDS\n(i
n particular generalising [Bouajjani\, J. Esparza\, and O. Maler 1997] and
\n [A. Finkel\, B. Willems\, and P. Wolper\, 1997]\, which operate on ordi
nary\npushdown automata).\n\nThis talk will present the ideas behind CSHOR
e\, a model-checking tool for HORS\nthat is based on CPDS saturation and w
hose performance is not completely\nunpromising!\n\nWe will also give an o
verview of the tool HorsSat(T)\, which implements\ntwo algorithms\, each o
f which uses saturation-like principles.\nIn contrast to CSHORe\, these op
erate directly on HORS (rather than CPDS) and\nadopt the more traditional
approach of using intersection types to reason\nabout their behaviour.\n\n
\n***CSHORe is joint work with Arnaud Carayol\, Matthew Hague and Olivier
Serre (to appear in ICFP 2013). HorsSat(T) is joint work with Naoki Kobaya
shi (to appear in CSL 2013)***\n
LOCATION:LMU main building\, A020
URL:http://www.model.in.tum.de/~frieling/2013-07-12-Broadbent.pdf
CONTACT:Broadbent Christopher
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094siCK@lapbroy149
DTSTART;TZID=Europe/Berlin:20090526T160000
DTEND;TZID=Europe/Berlin:20090526T170000
SUMMARY:Bouajjani Ahmed: Context-Bounded Analysis for Concurrent Programs w
ith Dynamic Creation of Threads
DESCRIPTION:Context-bounded analysis has been shown to be both efficient an
d effective at finding bugs in concurrent programs. According to its origi
nal definition\, context-bounded analysis explores all behaviors of a conc
urrent program up to some fixed number of context switches between threads
. This definition is inadequate for programs that create threads dynamical
ly because bounding the number of context switches in a computation also b
ounds the number of threads involved in the computation. In this paper\, w
e propose a more general definition of context-bounded analysis useful for
programs with dynamic thread creation. The idea is to bound the number of
context switches for each thread instead of bounding the number of switch
es of all threads. We consider several variants based on this new definiti
on\, and we establish decidability and complexity results for the analysis
induced by them.
LOCATION:TUM Garching - 02.07.014
CONTACT:Bouajjani Ahmed
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094T135@lapbroy149
DTSTART;TZID=Europe/Berlin:20110708T100000
DTEND;TZID=Europe/Berlin:20110708T110000
SUMMARY:Cook Byron: A new approach to temporal property verification
DESCRIPTION:In recent work we have found new approaches to the old problem
of automatic temporal property verification. As well as leading to drama
tic performance improvements\, this work also helps to clarify some age-ol
d questions about the connections between seemingly disparate historic app
roaches.
LOCATION:LMU\, Schellingstr. 5 - Room 204
CONTACT:Cook Byron
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094T4fN@lapbroy149
DTSTART;TZID=Europe/Berlin:20111028T083000
DTEND;TZID=Europe/Berlin:20111028T093000
SUMMARY:Li Xin: Precision & Scalability of Stacking-based Java Program Anal
ysis
DESCRIPTION:Pushdown systems (PDSs) are known to be natural models of progr
ams with\nrecursive procedures. However\, it pose new challenges to precis
ely and\nefficiently analyze large-scale programs with object-oriented fea
tures by PDSs.\nIn this talk\, I will introduce our efforts and preliminar
y results on designing\nprecise yet scalable stacking-based program analys
is for Java\, mainly including\nconditional weighted PDSs that enhance the
expressiveness of weighted PDSs and\nyield more precise Java program anal
ysis\, and a modular model checking\nalgorithm on weighted PDSs\, to reduc
e both time and memory cost of Java\npoints-to analysis in practice.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Li Xin
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094TDqd@lapbroy149
DTSTART;TZID=Europe/Berlin:20091215T100000
DTEND;TZID=Europe/Berlin:20091215T110000
SUMMARY:Durand-Gasselin Antoine: Non-deterministic automata for Presburger
Arithmetic
DESCRIPTION:The use of automata to decide Presburger Arithmetic (PA) has be
en\nintroduced by Buechi in 1960. Henceforth we represent PA's formula by
the\n(minimal deterministic finite) automaton that encodes its solutions\,
we\ntherefore have a canonic representation of PA's formula. We got\ninte
rested in the use of non-deterministic automata for Presburger\narithmetic
as they can be exponentially smaller.\n\nWe restrained ourselves to the c
lass of RFSA (residual finite state\nautomata -- automata for which the re
sidual language of each state is a\nresidual of the recognized langage)\,
for they also admit a canonical\nform which is computable and minimal w.r.
t. the number of states. We\ngive a compared study of the number of states
of the minimal\ndeterministic finite automaton and of the canonical RSFA\
, for some\nsimple fragments of PA.
LOCATION:TUM Garching - 01.09.014
CONTACT:Durand-Gasselin Antoine
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094u4mB@lapbroy149
DTSTART;TZID=Europe/Berlin:20130201T100000
DTEND;TZID=Europe/Berlin:20130201T110000
SUMMARY:Vogel-Heuser Birgit: Requirements for modeling and estimating runt
ime behavior in automation
LOCATION:Garching\, MI 02.07.014
CONTACT:Vogel-Heuser Birgit
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094u50I@lapbroy149
DTSTART;TZID=Europe/Berlin:20130301T100000
DTEND;TZID=Europe/Berlin:20130301T110000
SUMMARY:Albarghouthi Was: From SMT Solvers to Interpolators to Verifiers
DESCRIPTION:SMT solvers have become the standard tools underlying many\nsym
bolic execution engines and bounded model checkers. Whereas these\ntechniq
ues do not give guarantees on absence of errors\, it has been\nshown that
Craig interpolants mined from unsatisfiability proofs can\nbe used as gues
ses for inductive invariants (correctness proofs). In\nthis talk\, I will
describe our interpolation-based verification\ntechniques\, and how combin
ing interpolation with abstract\ninterpretation can be quite advantageous.
I will also describe our\nexperience implementing these techniques in the
UFO framework\, an\nopen-source C verification framework we built in the
LLVM compiler\ninfrastructure. This is joint work with Arie Gurfinkel (SEI
\, CMU) and\nMarsha Chechik (Univ. of Toronto).
LOCATION:Garching MI 02.07.014
URL:http://www.model.in.tum.de/~frieling/2013-03-Aws-Albarghouthi.pdf
CONTACT:Albarghouthi Was
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094uBEc@lapbroy149
DTSTART;TZID=Europe/Berlin:20110218T100000
DTEND;TZID=Europe/Berlin:20110218T110000
SUMMARY:Kuncak Viktor: Implicit Programming through Automated Reasoning
DESCRIPTION:We argue for a programming model where automated reasoning play
s\na key role during (1) interactive program development\, (2)\nprogram co
mpilation\, and (3) program execution. I will focus on\nour recent results
in complete functional synthesis for integer\narithmetic\, which is a for
m of program compilation based on\ndecision procedures. For program develo
pment\, I outline our\nongoing work on resolution theorem proving for inte
ractive\nsynthesis. For program execution\, I describe the UDITA system\nb
ased on Java Pathfinder\, and argue that programming models\nrelated to co
nstraint logic programming should play a bigger\nrole in mainstream softwa
re.\n* For more information\, please see:\n http://lara.epfl.ch/w/impro
LOCATION:TUM Garching\, Room 03.09.014\n
CONTACT:Kuncak Viktor
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094uPlm@lapbroy149
DTSTART;TZID=Europe/Berlin:20090226T160000
DTEND;TZID=Europe/Berlin:20090226T170000
SUMMARY:Friedmann Oliver: A Super-Polynomial Lower Bound for the Parity Gam
e Strategy Improvement Algorithm as We Know it.
DESCRIPTION:We present a new lower bound for the discrete strategy improvem
ent algorithm for solving parity games due to Voege and Jurdzinski. First\
, we informally show which structures are difficult to solve for the algor
ithm. Second\, we outline a family of games of quadratic size on which the
algorithm requires exponentially many strategy iterations\, answering in
the negative the long-standing question whether this algorithm runs in pol
ynomial time. Additionally we note that the same family of games can be us
ed to prove a similar result w.r.t. the strategy improvement variant by Sc
hewe.
LOCATION:LMU - Oettinger Str. 67\, room Z1.09
CONTACT:Friedmann Oliver
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094Uv7b@lapbroy149
DTSTART;TZID=Europe/Berlin:20130531T100000
DTEND;TZID=Europe/Berlin:20130531T110000
SUMMARY:Seidl Helmut: How to Combine Widening and Narrowing for Non-monoton
ic Systems of Equations.
DESCRIPTION:Non-trivial analysis problems require complete lattices\nwith i
nfinite ascending and descending chains. In order\nto compute reasonably p
recise post-fixpoints of the resulting\nsystems of equations\, Cousot and
Cousot have suggested accelerated\nfixpoint iteration by means of widening
and narrowing.\n\nThe strict separation into phases\, however\, may unnec
essarily give up\nprecision that cannot be recovered later. While widening
is also applicable\nif equations are non-monotonic\, this is no longer th
e case for narrowing.\nA narrowing iteration to improve a given post-fixpo
int\, additionally\,\nmust assume that all right-hand sides are monotonic.
\n\nThe latter assumption\, though\, is not met in presence of widening.\n
It is also not met by equation systems corresponding to context-sensitive\
ninterprocedural analysis\, possibly combining context-sensitive analysis
of\nlocal information with flow-insensitive analysis of globals.\n\nAs a r
emedy\, we present a novel operator that combines a given widening\noperat
or with a given narrowing operator. We present adapted versions\nof round-
robin as well as of worklist iteration\, local\, and\nside-effecting solvi
ng\nalgorithms for the combined operator and prove that the resulting\nsol
vers always\nreturn sound results and are guaranteed to terminate for mono
tonic systems\nwhenever only finitely many unknowns (constraint variables)
are encountered.
LOCATION:LMU main building\, A020
URL:http://www.model.in.tum.de/~frieling/2013-05-31-Seidl.pdf
CONTACT:Seidl Helmut
LAST-MODIFIED:20140313T143037Z
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094vFoD@lapbroy149
DTSTART;TZID=Europe/Berlin:20110617T083000
DTEND;TZID=Europe/Berlin:20110617T093000
SUMMARY:Patrick Regan: Engaging the World Beyond Your Field: communicating
with the media\, the public\, and other non-expert stakeholders.
DESCRIPTION:tba.
LOCATION:LMU Main Building - A U117
CONTACT:Patrick Regan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094viuE@lapbroy149
DTSTART;TZID=Europe/Berlin:20110603T083000
DTEND;TZID=Europe/Berlin:20110603T093000
SUMMARY:Jacobs Bart: VeriFast: a Powerful\, Sound\, Predictable\, Fast Veri
fier for C and Java
DESCRIPTION:VeriFast is a verifier for single-threaded and multithreaded C
and Java programs annotated with preconditions and postconditions written
in separation logic. To enable rich specifications\, the programmer may de
fine inductive datatypes\, primitive recursive pure functions over these d
atatypes\, and abstract separation logic predicates. To enable verificatio
n of these rich specifications\, the programmer may write lemma functions\
, i.e.\, functions that serve only as proofs that their precondition impli
es their postcondition. The verifier checks that lemma functions terminate
and do not have side-effects. Verification proceeds by symbolic execution
\, where the heap is represented as a separation logic formula. Since neit
her VeriFast itself nor the underlying SMT solver do any significant searc
h\, verification time is predictable and low. We are currently using VeriF
ast to verify fine-grained concurrent data structures\, unloadable kernel
modules\, and JavaCard programs. \n
LOCATION:LMU Main Building - A U117
CONTACT:Jacobs Bart
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094VRjo@lapbroy149
DTSTART;TZID=Europe/Berlin:20101209T171500
DTEND;TZID=Europe/Berlin:20101209T181500
SUMMARY:Leroux Jèrôme: Vector Addition System Reachability Problem (A Short
Self-Contained Proof)
DESCRIPTION:The reachability problem for Vector Addition Systems (VASs) is
a\ncentral problem of net theory. The general problem is known decidable\n
by algorithms exclusively based on the classical\nKosaraju-Lambert-Mayr-Sa
cerdote-Tenney decomposition (KLMTS\ndecomposition). Recently from this de
composition\, we deduced that a\nfinal configuration is not reachable from
an initial one if and only\nif there exists a Presburger inductive invari
ant that contains the\ninitial configuration but not the final one. Since
we can decide if a\nPreburger formula denotes an inductive invariant\, we
deduce from this\nresult that there exist checkable certificates of non-re
achability in\nthe Presburger arithmetic. In particular\, there exists a s
imple\nalgorithm for deciding the general VAS reachability problem based o
n\ntwo semi-algorithms. A first one that tries to prove the reachability\n
by enumerating finite sequences of actions and a second one that tries\nto
prove the non-reachability by enumerating Presburger formulas. In\nthis p
aper we provide the first proof of the VAS reachability problem\nthat is n
ot based on the KLMST decomposition. The proof is based on\nthe notion of
production relations inspired from Hauschildt that\ndirectly provides the
existence of Presburger inductive invariants.
LOCATION:00.08.038
CONTACT:Leroux JÃ©rÃ´me
LAST-MODIFIED:20140313T142805Z
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094Vshp@lapbroy149
DTSTART;TZID=Europe/Berlin:20120217T100000
DTEND;TZID=Europe/Berlin:20120217T110000
SUMMARY:Hoefner Peter: Formal Methods for Wireless Mesh Networks
DESCRIPTION:Wireless Mesh Networks (WMNs) have recently gained considerable
\npopularity and are increasingly deployed in a wide range of application\
nscenarios\, including emergency response communication\, intelligent\ntra
nsportation systems\, mining\, video surveillance\, etc. WMNs are\nessenti
ally self-organising wireless ad-hoc networks that can provide\nbroadband
communication without relying on a wired backhaul\ninfrastructure. This h
as the benefit of rapid and low-cost network\ndeployment. Traditionally\,
the main tools for evaluating and validating\nnetwork protocol are simulat
ion and test-bed experiments. The key\nlimitations of these approaches ar
e that they are very expensive\, time\nconsuming and non-exhaustive. As a
result\, protocol errors and\nlimitations are still found many years after
the definition and\nstandardisation.\nFormal methods have a great potenti
al in helping to address this\nproblem\, and can provide valuable tools fo
r the design\, evaluation and\nverification of WMN routing protocols. The
overall goal is to reduce the\n``time-to-market'' for better (new or modif
ied) WMN protocols\, and to\nincrease the reliability and performance of t
he corresponding networks.\n\nIn this talk I describe the importance of WM
Ns and present one of the\nleading protocols: the Ad-hoc on Demand Distanc
e Vector (AODV) routing\nprotocol.\nMoreover\, I give an overview over for
mal methods used so far to model\,\nanalyse and verify AODV.\nThis include
s a formal model using process algebra\, fully automation by\na matrix mod
el and the use of model checkers.\nIn an outlook I present some problems w
e are faced and discuss ongoing\nand future work. The latter includes a fo
rmal\nmodel of process algebra in Isabelle/HOL/.
LOCATION:TUM Garching - Room 01.11.018
CONTACT:Hoefner Peter
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094WFVc@lapbroy149
DTSTART;TZID=Europe/Berlin:20130628T100000
DTEND;TZID=Europe/Berlin:20130628T110000
SUMMARY:Heljanko Keijo: Using Unfoldings in Automated Testing of Multithrea
ded Programs
DESCRIPTION:In multithreaded programs both environment input data and the n
ondeterministic interleavings of concurrent events can affect the behavior
of the program. One approach to systematically explore the nondeterminism
caused by input data is dynamic symbolic execution. For testing multithre
aded programs we present a new approach that combines dynamic symbolic exe
cution with unfoldings\, a method originally developed for Petri nets but
also applied to many other models of concurrency. We provide an experiment
al comparison of our new approach with existing algorithms combining dynam
ic symbolic execution and partial-order reductions and show that the new a
lgorithm can explore the reachable control states of each thread with a si
gnificantly smaller number of test runs. In some cases the reduction to th
e number of test runs can be even exponential allowing programs with long
test executions or hard-to-solve constrains generated by symbolic executio
n to be tested more efficiently.\n\n\nThis is joint work with Kari Kaehkoe
nen and Olli Saarikivi
LOCATION:LMU main building\, A020
URL:http://www.model.in.tum.de/~frieling/2013-06-28-Heljanko.pdf
CONTACT:Heljanko Keijo
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094wWpF@lapbroy149
DTSTART;TZID=Europe/Berlin:20121214T100000
DTEND;TZID=Europe/Berlin:20121214T110000
SUMMARY:Kiefer Stefan: On the equivalence problem for probabilistic automat
a
DESCRIPTION:Deciding equivalence of probabilistic automata is a key problem
for\nestablishing various behavioural and anonymity properties of probabi
listic\nsystems. In particular\, it is at the heart of the tool APEX\, an
analyser\nfor probabilistic programs. APEX is based on game semantics and
analyses a\nbroad range of anonymity and termination properties of randomi
sed\nprotocols and other open programs.\n\nIn recent experiments a randomi
sed equivalence test based on polynomial\nidentity testing outperformed de
terministic algorithms. We show that\npolynomial identity testing yields e
fficient algorithms for various\ngeneralisations of the equivalence proble
m. First\, we provide a randomized\nNC procedure that also outputs a count
erexample trace in case of\ninequivalence. Second\, we consider equivalenc
e of probabilistic cost\nautomata. In these automata transitions are label
led with integer costs\nand each word is associated with a distribution on
costs\, corresponding to\nthe cumulative costs of the accepting runs on t
hat word. Two automata are\nequivalent if they induce the same cost distri
butions on each input word.\nWe show that equivalence can be checked in ra
ndomised polynomial time.\nFinally we show that the equivalence problem fo
r probabilistic visibly\npushdown automata is logspace equivalent to the p
roblem of whether a\npolynomial represented by an arithmetic circuit is id
entically zero.
LOCATION:Garching\, MI 02.07.014
CONTACT:Kiefer Stefan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094XhYT@lapbroy149
DTSTART;TZID=Europe/Berlin:20111209T083000
DTEND;TZID=Europe/Berlin:20111209T093000
SUMMARY:Mihaila Bogdan: Static Analysis of Binaries for Reverse Engineering
DESCRIPTION:The security of commercial software is determined by manually
\ninspecting the machine code of the software. Finding a security vulnerab
ility \nequates to singling out a fragment containing a handful of instru
ctions out of \nmillions and has been likened to finding the needle in th
e haystack. Our \nproject will equip the security engineer with tools to
automatically identify \ncode as free from vulnerabilities and to address
the construction of attacks \nfor dubious code fragments.\nIn order to ma
ke our tools scale\, we introduce a method to focus a \nforward static an
alysis on relevant parts of the program. This method is based \non recordi
ng a trace up to an interesting function f of the program under test \nand
then re-running this trace in the static analyser. The benefit is that f
\ncan be analysed with a small abstract context that is easier to comprehe
nd \nthan the actual program state and that is realistic in that it includ
es at \nleast one actual trace of the program.
LOCATION:TUM Garching - Room 02.07.014
CONTACT:Mihaila Bogdan
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094xji5@lapbroy149
DTSTART;TZID=Europe/Berlin:20101115T160000
DTEND;TZID=Europe/Berlin:20101115T170000
SUMMARY:Tuerk Thomas: Holfoot - a separation logic tool in HOL4
DESCRIPTION:I'm developing a separation logic framework based on Abstract S
eparation Logic inside the HOL4 theorem prover. This framework is instanti
ated to build Holfoot\, a formalisation of Smallfoot. In this talk\, I wil
l give a high-level presentation of Holfoot (http://holfoot.heap-of-proble
ms.org).\n\nSmallfoot (http://www.dcs.qmul.ac.uk/research/logic/theory/pro
jects/smallfoot) is an automated separation logic tool. It is able to reas
on about the partial correctness of programs written in a simple\, low-lev
el imperative language\, which is designed to resemble C. This language co
ntains pointers\, local and global variables\, dynamic memory allocation/d
eallocation\, conditional execution\, while-loops and recursive procedures
with call-by-value and call-by-reference arguments. Moreover\, concurrenc
y is supported by conditional critical regions and a parallel composition
operator. Smallfoot-specifications are concerned with the shape of datastr
uctures in memory. Their content is not considered.\n\nHolfoot can verify
most Smallfoot examples completely automatically. However\, it extends Sma
llfoot to reason about the content of datastructures. Moreover\, there is
support for arrays and pointer arithmetic. Considering the data-content al
lows Holfoot to reason about fully-functional specifications. Simple fully
-functional specifications like reversal of a single linked list can be ve
rified automatically. For more complicated examples like a fully-functiona
l specification of mergesort or insertion into a red-black-tree\, Holfoot
can be used interactively inside HOL4. This allows using all the libraries
and tools of HOL4.\n\n\nThis talk will be a high-level presentation of Ho
lfoot. I don't expect the audience to be familiar with separation logic or
HOL4. The talk will briefly sketch the semantic foundations\, i.e. Abstra
ct Separation Logic. Then\, an end-user view on Holfoot will be presented.
Holfoot's web-interface (http://holfoot.heap-of-problems.org/web-interfac
e.php) will be used to run Holfoot on concrete examples. I will also brief
ly demonstrate\, how to use Holfoot interactively inside the HOL4 theorem
prover to tackle more complicated specifications.
LOCATION:TUM Garching\, Room 00.09.055
URL:http://puma.in.tum.de/wiki/Puma_talk_thomas_tuerk
CONTACT:Tuerk Thomas
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094xNjl@lapbroy149
DTSTART;TZID=Europe/Berlin:20110520T083000
DTEND;TZID=Europe/Berlin:20110520T093000
SUMMARY:Kuncar Ondrej: Proving Valid Quanti?ed Boolean Formulas in HOL Ligh
t
DESCRIPTION:I am going to describe the integration of Squolem\, Quanti?ed\n
Boolean Formula (QBF) solver\, with the interactive theorem prover HOL\nLi
ght in my talk. Squolem generates certi?cates of validity\, which are\nbas
ed on Skolem functions as witnesses. The certi?cates are checked in\nHOL L
ight by constructing proofs based on these certi?cates. The\npresented app
roach allows HOL Light users to prove larger valid QBF\nproblems than befo
re and provides correctness checking of Squolem?s\noutputs based on the LC
F approach. An error in Squolem was discovered\nthanks to the integration.
Experiments show that the feasibility of the\nintegration is very sensiti
ve to implementation of HOL Light and used\ninferences. This resulted in i
mprovements in HOL Light?s inference kernel.
LOCATION:LMU Main Building - A U117
CONTACT:Kuncar Ondrej
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094xWjX@lapbroy149
DTSTART;TZID=Europe/Berlin:20130327T150000
DTEND;TZID=Europe/Berlin:20130327T160000
SUMMARY:Genaim Samir: On the Linear Ranking Problem for Integer Linear-Cons
traint Loops
DESCRIPTION:We study the complexity of the Linear Ranking problem: given a
loop\,\ndescribed by linear constraints over a finite set of integer\nvari
ables\, is there a linear ranking function for this loop? While\nexistence
of such a function implies termination\, this problem is not\nequivalent
to termination. When the variables range over the rationals\nor reals\, th
e Linear Ranking problem is known to be PTIME decidable.\nHowever\, when t
hey range over the integers\, whether for single-path or\nmultipath loops\
, the complexity of the Linear Ranking problem has not\nyet been determine
d. We show that it is coNP-complete. However\, we\npoint out some special
cases of importance of PTIME complexity. We\nalso present complete algori
thms for synthesizing linear ranking\nfunctions\, both for the general cas
e and the special PTIME cases.\n\n(joint work with Amir M. Ben-Amram)
LOCATION:Garching MI 02.07.014
URL:http://www.model.in.tum.de/~frieling/2013-03-Samir-Genaim.pdf
CONTACT:Genaim Samir
END:VEVENT
BEGIN:VEVENT
DTSTAMP:20140204T115814Z
UID:1391515094ztmM@lapbroy149
DTSTART;TZID=Europe/Berlin:20100510T160000
DTEND;TZID=Europe/Berlin:20100510T170000
SUMMARY:Stolz Volker: The rCOS Modeler -- from Software Engineering to Veri
fication
DESCRIPTION:In this presentation we give an overview of use case-driven dev
elopment of component- and object based system using Refinement of Compone
nt- and Object-base Systems\, rCOS. The tool supports model construction\,
analysis\, verification and correctness preserving transformations\, and
it generate verifiable code from design models.\nWe also report on a recen
t project of integrating Runtime Verification into the software engineerin
g process.
LOCATION:LMU Oettingerstr. 67\, 151
CONTACT:Stolz Volker
END:VEVENT
BEGIN:VEVENT
TRANSP:OPAQUE
DTEND;TZID=Europe/Berlin:20150508T100000
UID:1441-5538E280-8D-2CB11200
DTSTAMP:20150331T150240Z
LOCATION:LMU D Z007
DESCRIPTION:Population protocols (Angluin et al.\, 2006) are a formal model
of sensor networks consisting of identical mobile devices. When two devic
es come into the range of each other\, they interact and change their stat
es. Computations are infinite sequences of interactions satisfying a stron
g fairness constraint.\n\nA population protocol is well-specified if for e
very initial configuration $C$ of devices\, and every computation starting
at $C$\, all devices eventually agree on a consensus value depending only
on $C$. If a protocol is well-specified\, then it is said to compute the
predicate that assigns to each initial configuration its consensus value.\
n\nWhile the predicates computable by well-specified protocols have been e
xtensively studied\, the two basic verification problems remain open: is a
given protocol well-specified? Does a protocol compute a given predicate
? We prove that both problems are decidable.
SEQUENCE:6
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
SUMMARY:Javier Esparza: Verification of population protocols
DTSTART;TZID=Europe/Berlin:20150508T083000
LAST-MODIFIED:20150507T081407Z
CREATED:20150331T150240Z
END:VEVENT
BEGIN:VEVENT
UID:14CC-5623BF00-1-6FB57D80
SUMMARY:Manfred Kerber: Sound Auction Specification and Implementation usin
g Isabelle
LOCATION:TUM MI 02.07.014
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20151018T154635Z
DTSTAMP:20151018T154635Z
LAST-MODIFIED:20160108T214154Z
DTSTART;TZID=Europe/Berlin:20160108T100000
DTEND;TZID=Europe/Berlin:20160108T110000
TRANSP:OPAQUE
DESCRIPTION:We address two problems in auction design and practice: is a gi
ven auction design soundly specified\, possessing its intended properties\
; and\, is the design faithfully implemented when actually run? Failure on
either front can be hugely costly in large auctions. In the familiar sett
ing of the combinatorial Vickrey auction\, we use the Isabelle system to f
irst ensure that the auction has a set of desired properties (e.g. allocat
ing all items at non-negative prices)\, and to then generate verified exec
utable code directly from the specified design. Having established the exp
ected results in a known context\, we intend to use formal methods to veri
fy new auction designs.
ATTACH:https://www7.in.tum.de/~schulzef/2016-01-08-Manfred-Kerber.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:1518-555A0280-47-1E7D2D80
SUMMARY:Helmut Seidl: Equivalence of Deterministic Topdown Tree-to-string T
ransducers is decidable
LOCATION:LMU D Z007
DESCRIPTION:We show that equivalence of deterministic top-down tree-to-stri
ng transducers is decidable\, thus solving a long standing open problem in
formal language theory. We also present efficient algorithms for subclass
es: polynomial time for total transducers with unary output alphabet (over
a given top-down regular domain language)\, and co-randomized polynomial
time for linear transducers\; these results are obtained using techniques
from multi-linear algebra.\n\nFor our main result\, we prove that equivale
nce can be certified by means of inductive invariants using polynomial ide
als. This allows us to construct two semi-algorithms\, one searching for a
proof of equivalence\, one for a witness of non-equivalence.\n\n(Joint Wo
rk with Sebastian Maneth and Gregor Kemper)
CLASS:PUBLIC
CREATED:20150518T151728Z
DTSTAMP:20150518T151728Z
LAST-MODIFIED:20150527T092627Z
DTSTART;TZID=Europe/Berlin:20150522T083000
DTEND;TZID=Europe/Berlin:20150522T093000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2015-05-22-Helmut-Seidl.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:1778-537DD980-9-56371880
SUMMARY:Introducing LoLA 2.0: Explicit State Space Exploration for Petri Ne
ts by Karsten Wolf
LOCATION:LMU
DESCRIPTION:This is the first public presentation of a complete re-implemen
tation of\nthe LoLA (a LOw Level petrin net Analyzer) verification tool. U
sing this tool as an example\, we survey successful techniques in the area
of explicit state space verification. We demonstrate how (and where) to s
uccessfully apply these techniques.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:beyene@in.tum.de
CREATED:20140522T110556Z
DTSTAMP:20140522T110556Z
LAST-MODIFIED:20140614T092938Z
DTSTART;TZID=Europe/Berlin:20140613T083000
DTEND;TZID=Europe/Berlin:20140613T093000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
ATTACH:http://www.model.in.tum.de/~schulzef/2014-06-13-Karsten-Wolf.pdf
BEGIN:VALARM
TRIGGER;RELATED=START;VALUE=DURATION:-P3D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:1954-57FE2580-31-544B0500
SUMMARY:Matthias Volk: Analysis of Parametric Markov Chains
CLASS:PUBLIC
CREATED:20161012T115940Z
DTSTAMP:20161012T115940Z
LAST-MODIFIED:20161209T073034Z
DTSTART;TZID=Europe/Berlin:20161125T110000
DTEND;TZID=Europe/Berlin:20161125T120000
TRANSP:OPAQUE
SEQUENCE:3
LOCATION:TUM MI 02.07.034
DESCRIPTION:This talks presents our development in analyzing Parametric Mar
kov Chains (PMC). PMCs extend the well-known model of Discrete-Time Markov
Chains (DTMC) by allowing to leave open certain transition probabilities
and using parameters instead. The model checking goal then is to compute t
he probability of reaching certain target states which can be expressed as
a rational function over the parameters. We will discuss how to efficient
ly compute the exact rational function by use of a state elimination appro
ach. For better scalability\, a second approximate approach transforms the
PMC into a Markov Decision Process (MDP) and yields lower and upper bound
s on the resulting probability. Both approaches can be used for the parame
ter synthesis problem: given a probability threshold\, find sound paramete
r values ensuring this threshold. Here we make use of SMT solving techniqu
es to partition the parameter space into safe and unsafe regions satisfyin
g or rejecting the given threshold.
ATTACH:https://www7.in.tum.de/~schulzef/2016-11-25-Matthias-Volk.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:1AF9-54816A80-8B-14248360
SUMMARY:Deepak D'Souza: Shape Analysis for Concurrent Programs
LOCATION:TUM MI 02.07.014
DESCRIPTION:Shape analysis is a program analysis technique based on abstrac
t interpretation that aims to find invariants on the shape of heap data-st
ructures maintained by the program. Our aim in this talk to describe an ef
ficient way of doing shape analysis for concurrent (or multi-threaded) pro
grams. The main idea is to decompose the heap into regions that are access
ed in a mutually-exclusive manner by the threads\, to track the shape of t
hese regions separately\, and propagate facts about them only along synchr
onization points between the threads.\n\nThis is joint-work (in-progress!)
with Arnab De and Suvam Mukherjee.
CLASS:PUBLIC
CREATED:20141205T081811Z
DTSTAMP:20141205T081811Z
LAST-MODIFIED:20141205T081959Z
DTSTART;TZID=Europe/Berlin:20141219T100000
DTEND;TZID=Europe/Berlin:20141219T110000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:1C56-555B1A00-19-2AF6B1C0
SUMMARY:Matthias Althoff: Modeling and Simulation of Continuous Systems
LOCATION:LMU D Z007
DESCRIPTION:In many modern systems\, computing elements are tightly connect
ed with physical entities for which the term cyber-physical systems has be
en established in recent years. Examples are automated vehicles\, surgical
robots\, smart grids\, and collaborative human-robot manufacturing. This
lecture series (three lectures) provides the attendees with the required b
asics to extend formal verification techniques from discrete systems to hy
brid systems (mixed discrete and continuous dynamics).\n\n- Ordinary diffe
rential equations\n- Analytical solution of ordinary differential equation
s\n- Numerical solution of ordinary differential equations
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150519T111246Z
DTSTAMP:20150519T111246Z
LAST-MODIFIED:20150612T133149Z
DTSTART;TZID=Europe/Berlin:20150529T083000
DTEND;TZID=Europe/Berlin:20150529T093000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2015-05-29-Matthias_Althoff-PUMA_CP
S_part1_ModelingAndSimulationOfContinousSystems.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:1C56-555B1B00-21-2AF6B1C0
SUMMARY:Matthias Althoff: Timed Automata + Modeling and Simulation of Hybri
d Systems
LOCATION:LMU D Z007
DESCRIPTION:In many modern systems\, computing elements are tightly connect
ed with physical entities for which the term cyber-physical systems has be
en established in recent years. Examples are automated vehicles\, surgical
robots\, smart grids\, and collaborative human-robot manufacturing. This
lecture series (three lectures) provides the attendees with the required b
asics to extend formal verification techniques from discrete systems to hy
brid systems (mixed discrete and continuous dynamics).\n\n- Stability anal
ysis of hybrid systems\n- Reachability analysis of hybrid systems\n- Appli
cations
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150519T111440Z
DTSTAMP:20150519T111440Z
LAST-MODIFIED:20150612T133240Z
DTSTART;TZID=Europe/Berlin:20150605T083000
DTEND;TZID=Europe/Berlin:20150605T093000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2015-06-05-Matthias_Althoff-PUMA_CP
S_part2_TimedAutomata.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:1C56-555B1B00-29-2AF6B1C0
SUMMARY:Matthias Althoff: Analysis of Hybrid Systems
LOCATION:LMU D Z007
DESCRIPTION:In many modern systems\, computing elements are tightly connect
ed with physical entities for which the term cyber-physical systems has be
en established in recent years. Examples are automated vehicles\, surgical
robots\, smart grids\, and collaborative human-robot manufacturing. This
lecture series (three lectures) provides the attendees with the required b
asics to extend formal verification techniques from discrete systems to hy
brid systems (mixed discrete and continuous dynamics).\n\n- Stability anal
ysis of hybrid systems\n- Reachability analysis of hybrid systems\n- Appli
cations
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150519T111523Z
DTSTAMP:20150519T111523Z
LAST-MODIFIED:20150612T140631Z
DTSTART;TZID=Europe/Berlin:20150612T083000
DTEND;TZID=Europe/Berlin:20150612T093000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2015-06-12-Matthias_Althoff-PUMA_CP
S_part3_and_4_AnalysisOfHybridSystems.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:1CDB-5575CE80-7-242B2C0
SUMMARY:Ann-Christin Knoll: Decision Procedures for the Monadic Fragment an
d Guarded Negation Fragment in SPASS
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150608T171946Z
DTSTAMP:20150608T171946Z
LAST-MODIFIED:20150707T101851Z
DTSTART;TZID=Europe/Berlin:20150710T083000
DTEND;TZID=Europe/Berlin:20150710T093000
TRANSP:OPAQUE
LOCATION:LMU D Z007
SEQUENCE:2
DESCRIPTION:The monadic fragment and guarded negated fragment are two decid
able fragments of first-order logic. The monadic fragment has\nbeen known
for a long time and decision procedures have already been implemented [Har
12]. The guarded negation fragment however\nhas been more recently introdu
ced. Though proven to be decidable [BtCS11]\, no decision procedure has ye
t been presented nor imple-\nmented. This talk gives an overview of clause
s classes and decision procedures formed for the monadic fragment using th
e approaches of splitting and condensing in combination with ordered resol
ution. Their implementation will be demonstrated in the automated theorem
prover SPASS 1 . Furthermore it covers ideas and experiments made to defin
e clauses classes and to find a decision procedure for the guarded negated
fragment. Since this is an active area of research the outcome cannot exa
ctly be predicted but there will definitely be some problems and challenge
s to overcome and hopefully some solutions found.\n
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20140416T122515Z
LAST-MODIFIED:20140417T130206Z
DTSTAMP:20140417T130206Z
UID:20140313T113842CET-7709Bvedib@131.159.22.15
SUMMARY:Rizaldi Albert: Logic and Verification of Markov Automata
CATEGORIES:PUMA Events
DTSTART;TZID=Europe/Berlin:20140303T103000
DTEND;TZID=Europe/Berlin:20140303T110000
LOCATION:TUM Garching - 02.07.014
TRANSP:OPAQUE
SEQUENCE:1
X-MOZ-GENERATION:4
END:VEVENT
BEGIN:VEVENT
UID:20140313T113842CET-7713OahU1r@131.159.22.15
DTSTAMP:20140313T103842Z
CATEGORIES:PUMA Events
DTSTART;TZID=Europe/Berlin:20140303T100000
DURATION:PT1H0M0S
LOCATION:TUM Garching - 02.07.014
SUMMARY:Rizaldi Albert: Modelling Environment of Insulin Pumps in Event-B.
DTEND;TZID=Europe/Berlin:20140303T103000
LAST-MODIFIED:20140313T135609Z
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:20140313T113842CET-7716AuSrlR@131.159.22.15
DTSTAMP:20140313T103842Z
CATEGORIES:PUMA Events
DTSTART;TZID=Europe/Berlin:20140207T100000
DURATION:PT1H0M0S
LOCATION:TUM Garching - 02.07.014
SUMMARY:König Barbara: Behavioural Metrics - A Coalgebraic Approach
DTEND;TZID=Europe/Berlin:20140207T100000
LAST-MODIFIED:20140313T142417Z
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:2428-534BB500-B-2B0293C0
SUMMARY:Utilisation of formal methods for cyber security at FireEye
LOCATION:TUM Garching - FMI 01.11.018
DESCRIPTION:The talk will first provide some background information about t
he challenges of\noperating-system verification and the results achieved s
o far. I will then\npresent FireEye's approach for improving cyber securit
y. Finally\, I introduce\nthe new research and development center at Dresd
en and talk about our goal to\nuse formal methods to further improve FireE
ye's products.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:beyene@in.tum.de
CREATED:20140414T101624Z
DTSTAMP:20140414T101624Z
LAST-MODIFIED:20140414T101624Z
DTSTART;TZID=Europe/Berlin:20140509T140000
DTEND;TZID=Europe/Berlin:20140509T150000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
END:VEVENT
BEGIN:VEVENT
UID:2428-534BB600-13-2B0293C0
SUMMARY:Treffen mit Siemens im PUMA Graduiertenkolleg
LOCATION:TUM Garching\, room MI 02.07.014
DESCRIPTION:Wir betrachten ein verteiltes System an Steuergeräten und betre
iben\ndieses als nicht-funktionale Plattform. Das bedeutet\, dass auf dies
er\nMengen an Steuergeräten beliebige Fahr- und Assistenzfunktionen\ninsta
lliert und zusätzliche Steuergeräte ins Netzwerk eingebracht werden\nkönne
n. Eine SW-Schicht (RTE = Runtime Environment) gewährleistet alle\nnicht-f
unktionalen Eigenschaften des Datenaustauschs zwischen Fahr- und\nAssisten
zfunktionen sowie deren Ausführung.\n\nDie RTE entkoppelt die funktionale
von der physikalischen Schicht und\nkapselt Mechanismen mit dem Ziel nicht
-funktionale Qualitäten\nsicherzustellen. Jenseits der RTE betrachten wir
eine Sensordatenfusion\nsowie ein Fahrzeug- und Umgebungsmodell.\n\nIn all
en drei Bereichen würden wir gerne prüfen\, in wie weit Methoden\nder form
alen Verifkation Anwendung finden können.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:beyene@in.tum.de
CREATED:20140414T101917Z
DTSTAMP:20140414T101917Z
LAST-MODIFIED:20140515T141627Z
DTSTART;TZID=Europe/Berlin:20140519T150000
DTEND;TZID=Europe/Berlin:20140519T160000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:253D-58330200-1-44202A00
SUMMARY:Tobias Heindel: Average motif counts in Markov chains of graph tran
sformation systems
LOCATION:TUM MI 00.09.038
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20161121T141819Z
DTSTAMP:20161121T141819Z
LAST-MODIFIED:20170104T094744Z
DTSTART;TZID=Europe/Berlin:20161216T100000
DTEND;TZID=Europe/Berlin:20161216T110000
TRANSP:OPAQUE
DESCRIPTION:The dynamics of the average molecule count of a chemical specie
s in a test tube over time is the paradigm example for motif counts in con
tinuous-time systems with countable state space. More generally\, we can c
onsider average counts of “observable” graph motifs in Markov processes th
at are specified by graph transformation systems (GTS)\; chemical reaction
s are a special case. Further applications of such average counts are meas
uring network flows\, protein production in cells\, and speed of DNA-walke
rs.\n\nComputing expected values of motif counts is typically extremely co
mplicated if possible at all\; it often amounts to solving the master equa
tion of the underlying Markov chain with countable state space to suitable
precision. The case is much different if we restrict to the graph transfo
rmation analogue of context-free Chomsky grammars\, namely context-free GT
Ss\, aka hyper-edge replacement systems. For these systems\, it is always
possible to construct for each motif of interest a finite ordinary differe
ntial equation (ODE) that captures the time evolution of the average count
of the motif precisely. To illustrate the analysis technique using ODEs\,
the preferential attachment process\, a popular model in the context of
citation networks\, will feature as running example. Time permitting\, iss
ues of the general graph transformation case and the main ideas of how to
resolve them will be overviewed.
ATTACH:https://www7.in.tum.de/~schulzef/2016-12-16-Tobias-Heindel.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:25D2-57038580-81-3DCE8340
SUMMARY:Stefan Hetzl: Inductive theorem proving based on tree grammars
LOCATION:TUM MI 03.09.014
DESCRIPTION:This talk is about an approach to inductive theorem proving whi
ch is based on recent proof-theoretic results on the relationship between
induction and tree grammars.\n\nThese results suggest an algorithm for pro
ving universal statements by induction which proceeds in two phases: the f
irst phase consists of a structural analysis of proofs of instances of the
universal statement. The result of such an analysis is a certain type of
tree grammar which induces a quantifier-free Boolean unification problem.
Each solution to this problem is an induction invariant. The second phase
consists of finding a solution of this unification problem.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160405T093410Z
DTSTAMP:20160405T093410Z
LAST-MODIFIED:20160411T130003Z
DTSTART;TZID=Europe/Berlin:20160406T100000
DTEND;TZID=Europe/Berlin:20160406T110000
TRANSP:OPAQUE
SEQUENCE:1
ATTACH:https://www7.in.tum.de/~schulzef/2016-04-06-Stefan-Hetzl.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:2656-54608300-1-6C6BD900
SUMMARY:Peter Habermehl: Logics and Automata for Multi-attributed Data Word
s
LOCATION:TUM MI 02.07.014
DESCRIPTION:We consider temporal logics on multi-attributed data words whic
h are words over a finite alphabet where each position additionally carrie
s multiple data values from an infinite domain. Multi-attributed data word
s can model naturally executions of object-oriented or parallel systems. R
ecently\, BD-LTL was introduced as a temporal logic on data words extendin
g LTL by navigation along positions of single data values. Allowing naviga
tion wrt. tuples of data values makes the satisfiability problem undecidab
le. We therefore introduce ND-LTL\, an extension of BD-LTL by a restricted
form of tuple-navigation. We study several of its fragments and obtain se
veral decidability results. The proof techniques are based on translating
the satisfiability problems to the emptiness problem of several classes of
Data Automata whose emptiness\nproblems are then further translated into
reachability or coverability problems on counter automata.\n\nBased on joi
nt work with N. Decker\, M. Leucker and D. Thoma from University Lübeck.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20141110T092050Z
DTSTAMP:20141110T092050Z
LAST-MODIFIED:20141208T151339Z
DTSTART;TZID=Europe/Berlin:20141205T100000
DTEND;TZID=Europe/Berlin:20141205T110000
TRANSP:OPAQUE
SEQUENCE:1
ATTACH:http://www.model.in.tum.de/~schulzef/2014-12-05-Peter-Habermehl.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:2BC6-570B5600-1-2E4C8540
SUMMARY:Max Haslbeck: Verified Analysis of List Update Algorithms
LOCATION:TUM MI 00.09.038
DESCRIPTION:We present a formalized quantitative analysis of a number of cl
assical algorithms for the list update problem: 2-competitiveness of move-
to-front\, the lower bound of 2 for the competitiveness of deterministic l
ist update algorithms and 1.6-competitiveness of the randomized COMB algor
ithm\, the best randomized list update algorithm known to date.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160411T074624Z
DTSTAMP:20160411T074624Z
LAST-MODIFIED:20160411T074624Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20160418T140000
DTEND;TZID=Europe/Berlin:20160418T150000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:2C3D-56011700-15-4B64C180
SUMMARY:Jan Krcal: Scalable Analysis of Fault Trees with Dynamic Features
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150922T085441Z
DTSTAMP:20150922T085441Z
LAST-MODIFIED:20151221T170057Z
DTSTART;TZID=Europe/Berlin:20151211T100000
DTEND;TZID=Europe/Berlin:20151211T110000
TRANSP:OPAQUE
LOCATION:TUM MI 02.07.014
DESCRIPTION:Fault trees constitute one of the essential formalisms for stat
ic safety analysis of various industrial systems. Dynamic fault trees (DFT
) enrich the formalism by time-dependent behaviour\, e.g.\, repairs or fun
ctional dependencies. Analysis of DFT is so far limited to substantially s
maller models than those required for\, e.g.\, nuclear power plants. \n\nW
e propose a fault tree formalism that combines both static and dynamic fea
tures\, called SD fault trees. We introduce an analysis algorithm for an i
mportant subclass of SD fault trees. The algorithm (1) scales similarly to
static algorithms and (2) allows for a more realistic analysis compared t
o static algorithms as it takes into account temporal interdependencies. F
inally\, we demonstrate the applicability of the method by an experimental
evaluation on fault trees of nuclear power plants.
SEQUENCE:1
ATTACH:https://www7.in.tum.de/~schulzef/2015-12-11-Jan-Krcal.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:318D-564C9380-2D-54307000
SUMMARY:Stefan Wagner: Empirical Results on Cloning and Clone Detection
LOCATION:TUM MI 02.07.014
DESCRIPTION:Cloning means the use of copy-paste as method in developing sof
tware artefacts. This practice has several problems\, such as unnecessary
increase of these artefacts\, and thereby increased comprehension and chan
ge efforts\, as well as potential inconsistencies. The automatic detection
of clones has been a topic for research for several years now and we have
made huge progress in terms of precision and recall. This led to a series
of empirical analyses we have performed on the effects and the amount of
cloning in code\, models and requirements. We continue to investigate the
effects of cloning and work on extending clone detection to functionally s
imilar code. This talk will give insights into how clone detection works a
nd the empirical results we have gathered.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20151118T150615Z
DTSTAMP:20151118T150615Z
LAST-MODIFIED:20151211T140751Z
DTSTART;TZID=Europe/Berlin:20151127T100000
DTEND;TZID=Europe/Berlin:20151127T110000
TRANSP:OPAQUE
ATTACH:https://www.stefan-wagner.biz/new-events/2015/11/27/vortrag-bei-der-
graduiertenschule-puma
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:318E-537E3F00-9-1944D1C0
SUMMARY:Two Worlds Apart: Bridging the Gap Between Physical and Cyber World
s by Majid Zamani
LOCATION:LMU room E 210\, Geschw.-Scholl-Pl. 1 (E)
DESCRIPTION:The tight interaction of computational systems within the physi
cal world\, known as Cyber-Physical Systems (CPSs)\, is believed to carry
great promises for the competitiveness of many safety critical industries.
Examples of such safety critical systems include aerospace\, chemical pro
cesses\, automotive\, energy\, robotics\, healthcare\, etc. Within CPSs\,
embedded control software plays a significant role by monitoring and adjus
ting several physical variables through feedback loops. Although CPSs have
become ubiquitous in modern technology\, the design of embedded control s
oftware is still based on ad-hoc solutions. In order to detect and elimina
te embedded design flaws\, a large portion of the design budget is consume
d with validation and verification tests. In this talk\, I will propose a
new approach for the design of embedded control software by changing the e
mphasis from verification to design. I will show that it is possible to sy
nthesize correct-by-design embedded control software for CPSs while provid
ing formal guarantees of correctness and preventing the need for costly po
st facto verifications. In particular\, I will show our techniques on the
synthesis of correct-by-design embedded control software enforcing discret
e specifications on (stochastic) continuous systems. Case studies from ene
rgy systems and motion planning will be employed to elucidate the results.
\n\n\nBiography:\nMajid Zamani is an assistant professor in the Department
of Electrical Engineering and Information Technology at Technische Univer
sität München where he leads the Hybrid Control Systems Group. He received
a Ph.D. degree in Electrical Engineering and an MA degree in Mathematics
both from University of California\, Los Angeles in 2012\, an M.Sc. degree
in Electrical Engineering from Sharif University of Technology in 2007\,
and a B.Sc. degree in Electrical Engineering from Isfahan University of Te
chnology in 2005. From September 2012 to December 2013\, he was a postdoct
oral researcher in the Delft Centre for Systems and Control at Delft Unive
rsity of Technology. Between December 2013 and May 2014\, he was an assist
ant professor in the Design Engineering Department at Delft University of
Technology.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:beyene@in.tum.de
CREATED:20140522T181840Z
DTSTAMP:20140522T181840Z
LAST-MODIFIED:20140702T083207Z
DTSTART;TZID=Europe/Berlin:20140704T083000
DTEND;TZID=Europe/Berlin:20140704T093000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
BEGIN:VALARM
TRIGGER;RELATED=START;VALUE=DURATION:-P3D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:33A6-53A1A600-1-6EC6D480
SUMMARY:An SMT-based Approach to Coverability Analysis by Philipp Meyer
LOCATION:LMU room E 210\, Geschw.-Scholl-Pl. 1 (E)
DESCRIPTION:Model checkers based on Petri net coverability have been used\n
successfully in recent years to verify safety properties of concurrent\nsh
ared-memory or asynchronous message-passing software. We revisit a\nconstr
aint approach to coverability based on classical Petri net\nanalysis techn
iques. We show how to utilize an SMT solver to implement\nthe constraint a
pproach\, and additionally\, to generate an inductive\ninvariant from a sa
fety proof. We empirically evaluate our procedure\non a large set of exist
ing Petri net benchmarks. Even though our\ntechnique is incomplete\, it ca
n quickly discharge most of the safe\ninstances. Additionally\, the induct
ive invariants computed are usually\norders of magnitude smaller than thos
e produced by existing solvers.\n\nJoint work with Javier Esparza\, Ruslán
Ledesma-Garza\, Rupak Majumdar\nand Filip Niksi\, to appear in CAV 2014.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:beyene@in.tum.de
CREATED:20140618T144856Z
DTSTAMP:20140618T144856Z
LAST-MODIFIED:20140618T144856Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20140627T083000
DTEND;TZID=Europe/Berlin:20140627T093000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:3852-55F7F280-1F-595D2580
SUMMARY:Alexandra Silva: NetKAT: A FORMAL SYSTEM FOR THE VERIFICATION OF NE
TWORKS
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150915T102838Z
DTSTAMP:20150915T102838Z
LAST-MODIFIED:20151112T163417Z
DTSTART;TZID=Europe/Berlin:20151016T100000
DTEND;TZID=Europe/Berlin:20151016T110000
TRANSP:OPAQUE
DESCRIPTION:NetKAT is a relatively new programming language and logic for\n
reasoning about packet switching networks that fits well with the\npopular
software defined networking (SDN) paradigm. NetKAT was\nintroduced quite
recently by Anderson et al. (POPL 2014) and further\ndeveloped by Foster e
t al. (POPL 2015). The system provides\ngeneral-purpose programming constr
ucts such as parallel and sequential\ncomposition\, conditional tests\, an
d iteration\, as well as\nspecial-purpose primitives for querying and modi
fying packet headers\nand encoding network topologies. The language allows
the desired\nbehavior of a network to be specified equationally. It has a
formal\ncategorical semantics and a deductive system that is sound and\nc
omplete over that semantics\, as well as an efficient decision\nprocedure
for the automatic verification of equationally-defined\nproperties of netw
orks.
ATTACH:https://www7.in.tum.de/~schulzef/2015-10-16-Silva.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:3944-55B24A80-15-490C6A80
SUMMARY:Maximilian Claus: Model Checking With Higher-Order Automated Theore
m Provers – A Logic Embedding Approach
LOCATION:TUM MI 02.07.014
DESCRIPTION:A model checker takes two inputs: a model description (here: a
finite-state imperative program) and a\nputative property\, which it shall
then verify. The logics in which these properties are stated\, such as li
near\ntemporal logic (LTL) or computation tree logic (CTL)\, are usually h
ard-wired into the model checker to allow\nfor the use of a heavily optimi
sed decision procedure. State-of-the-art examples include Spin [1] (for LT
L)\, which\nuses an automaton-based approach\, and SMV [2] (for CTL)\, whi
ch relies on an encoding of transition relations\nthrough binary decision
diagrams. I present a tool which is more flexible: It takes an imperative
program\, but\ntogether with a description of a freely chosen verification
logic\, stated as an embedding in classical higher-order\nlogic (HOL).\nE
mbeddings of modal logic in HOL have been used successfully before\, to so
lve a number of different problems\nas in [3] or [4]. From the embedding a
nd the model description the program generates a conjecture\, in THF0\nsyn
tax [5]\, to be proven by a higher-order automated theorem prover\, such a
s LEO-II [6] or Satallax [7]. The\nconjecture is a theorem if and only if
the input program is a model with the desired property.\nFor verifying rea
l-world models\, such an approach is so far prohibitively inefficient\, bu
t it still can give rise\nto a handful of interesting applications: It can
be used as a prototyping tool to quickly implement a verification\nlogic
of interest\, and it can provide sanity checks to see if the semantics of
a newly developed logic are correct.\nApart from that\, it might also be u
sed to easily create benchmark problems for theorem provers from simple\np
roblems in software verification.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150724T142510Z
DTSTAMP:20150724T142510Z
LAST-MODIFIED:20150724T142532Z
DTSTART;TZID=Europe/Berlin:20150729T090000
DTEND;TZID=Europe/Berlin:20150729T100000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:3C68-53638A00-1-5FEAE580
SUMMARY:Jane Hillston: Fluid Approximation for the Analysis of Collective S
ystems
LOCATION:TUM MI 02.07.014
DESCRIPTION:Stochastic process algebras have been used for more than 20 yea
rs for the formal description and analysis of quantitative aspects of syst
em behaviour. However\, like all discrete state representations\, they su
ffer from problems of state space explosion\, meaning that analysis become
s intractable as the size of the system grows. Nevertheless a process alg
ebra has many attractive features for modelling collective systems which c
onsist of multiple instances f simple components interacting as population
s.\n\nIn this talk I will briefly introduce the stochastic process algebra
PEPA and review its Markovian semantics which can be used to study aspect
s of dynamic behaviour. I will then explain how these semantics may be ri
gorously approximated\, in the case of collective systems\, by a set of or
dinary differential equations. These equations which are more efficient t
o analyse and are scale-free\, in the sense that the equations remain the
same as the populations grow.
CLASS:PUBLIC
CREATED:20140502T120534Z
DTSTAMP:20140502T120534Z
LAST-MODIFIED:20140723T200836Z
DTSTART;TZID=Europe/Berlin:20140723T160000
DTEND;TZID=Europe/Berlin:20140723T170000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
SEQUENCE:3
ATTACH:http://www.model.in.tum.de/~schulzef/2014-07-23-Jane-Hillston.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:3CA-54D09880-61-7144DA00
SUMMARY:Wilayat Khan: Client-side enforcement of web session integrity thro
ugh secure multi-execution
LOCATION:TUM MI 01.09.014
DESCRIPTION:Sessions on the web are fragile. They have been attacked succes
sfully in many ways\, by network-level attacks\, by direct attacks on sess
ion cookies (the main mechanism for implementing the session concept) and
by application-level attacks where the integrity of sessions is violated b
y means of cross-site request forgery or malicious script inclusion.\n\nIn
this talk\, a variant of non-interference is introduced - that can be use
d to formally define the notion of client-side application - level web ses
sion integrity. The work also develops and proves correct an enforcement m
echanism. Combined with state-of-the-art countermeasures for network-level
and cookie-level attacks\, this enforcement mechanism gives very strong a
ssurance about the client-side preservation of session integrity for authe
nticated sessions.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150203T094550Z
DTSTAMP:20150203T094550Z
LAST-MODIFIED:20150203T094550Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20150216T093000
DTEND;TZID=Europe/Berlin:20150216T101500
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:3E3C-56090080-595-4FCD1B80
SUMMARY:Stefan Kiefer: On the total variation distance of labelled Markov c
hains
LOCATION:TUM MI 02.07.014
DESCRIPTION:Labelled Markov chains (LMCs) are widely used in probabilistic
verification\, speech recognition\, computational biology\, and many othe
r fields. Checking two LMCs for equivalence is a classical problem subjec
t to extensive studies\, while the total variation distance provides a n
atural measure for the ``inequivalence'' of two LMCs: it is the maximum d
ifference between probabilities that the LMCs assign to the same event. W
e develop a theory of the total variation distance between two LMCs\, with
emphasis on the algorithmic aspects: (1) we provide a polynomial-time a
lgorithm for determining whether two LMCs have distance 1\, i.e.\, whether
they can almost always be distinguished\; (2) we provide an algorithm fo
r approximating the distance with arbitrary precision\; and (3) we show t
hat the threshold problem\, i.e.\, whether the distance exceeds a given
threshold\, is NP-hard and hard for the square-root-sum problem. We also
make a connection between the total variation distance and Bernoulli conv
olutions.\nJoint work with Taolue Chen.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150928T085547Z
DTSTAMP:20150928T085547Z
LAST-MODIFIED:20151005T065433Z
DTSTART;TZID=Europe/Berlin:20151002T100000
DTEND;TZID=Europe/Berlin:20151002T110000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2015-10-02-Stefan-Kiefer.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4176-5491D400-1-7A89068
SUMMARY:Javier Esparza: Parameterized Verification of Asynchronous Shared-M
emory Systems
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20141217T190620Z
DTSTAMP:20141217T190620Z
LAST-MODIFIED:20150116T130419Z
DTSTART;TZID=Europe/Berlin:20150109T100000
DTEND;TZID=Europe/Berlin:20150109T110000
TRANSP:OPAQUE
LOCATION:TUM MI 02.07.014
DESCRIPTION:We characterize the complexity of the safety verification probl
em for\nparameterized systems consisting of a leader process and arbitrari
ly many\nanonymous and identical contributors. Processes communicate thro
ugh a \nshared\, bounded-value register. There is no synchronization prim
itive to \nexecute a sequence of operations atomically. The model is inspi
red by \ndistributed algorithms implemented on sensor\nnetworks.\n\nWe ana
lyze the complexity of the safety verification problem when processes arem
odeled by finite-state machines\, pushdown machines\, and Turing machines.
Our\nproofs use combinatorial characterizations of\ncomputations in the m
odel\, and in case of pushdown-systems\, some novel\nlanguage-theoretic co
nstructions of independent interest.\n\nThis is joint work with Pierre Gan
ty and Rupak Majumdar.
SEQUENCE:1
ATTACH:https://www7.in.tum.de/~schulzef/2015-01-09-Javier-Esparza.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4176-5491D480-15-7A89068
SUMMARY:Javier Esparza: Deterministic Negotiations: Concurrency for Free
CLASS:PUBLIC
CREATED:20141217T190634Z
DTSTAMP:20141217T190634Z
LAST-MODIFIED:20150122T135007Z
DTSTART;TZID=Europe/Berlin:20150116T100000
DTEND;TZID=Europe/Berlin:20150116T110000
TRANSP:OPAQUE
LOCATION:TUM MI 02.07.014
DESCRIPTION:Negotiations are a model of concurrency close to Petri nets\, w
ith multiparty negotiation as\nprimitive. A negotiation is sound if\, what
ever the current state\, there is always a continuation\nleading to proper
termination.\n\nWe recall previous work in which we have designed a comp
lete set of reduction rules for \nso called deterministic negotiations tha
t allow one to analyze soundness of negotiations\nwithout explicitely cons
tructing the (possibly exponentially larger) state space\, \nWe then prese
nt a programming notation and show that it captures exactly the sound \nde
terministic negotiations.
SEQUENCE:1
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4192-58B94A00-35-5D7C9A00
SUMMARY:David de Frutos: Understanding (Concurrent) Process Semantics [seco
nd talk]
DESCRIPTION:Once asynchronous parallellsm induces non-determinism\, the sem
antics of concurrent systems becomes difficult to precise. Several framewo
rks to state that semantics have been considered\, and in any one of them
a lot of different semantics have been proposed. In our seminar we will pr
esent a unified approach\, where all these semantics can be presented\, so
that the differences and similarities between them can be captured in an
easy way. Besides\, this unified approach allows generic studies where the
properties of all the semantics can be stated and proved once and for all
\, thus avoiding the disturbing repetitions of the same arguments that we
usually find in the literature\, when any of these semantics is studied in
isolation.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170303T104949Z
DTSTAMP:20170303T104949Z
LAST-MODIFIED:20170324T161939Z
DTSTART;TZID=Europe/Berlin:20170320T150000
DTEND;TZID=Europe/Berlin:20170320T163000
TRANSP:OPAQUE
SEQUENCE:2
LOCATION:TUM MI 00.09.038
ATTACH:https://www7.in.tum.de/~schulzef/2017-03-20-David-de-Frutos.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4328-57C53200-1-456FFC80
SUMMARY:Julia Krämer: The Value of Attack-Defence Diagrams
LOCATION:TUM 02.07.014
DESCRIPTION:In an increasingly connected world\, formal specification and v
erification of cost-intensive and mission-critical cyber-physical systems
have become a crucial element of design processes both in industry and res
earch. Especially in the area of security-critical systems\, such as power
plants and water supply works\, the application of these techniques can s
ave not only costs but also human lives.\n\nSecurity-critical systems focu
s on robustness against attacks of malicious intruders\, which\, for insta
nce\, try to change the behaviour of the system or to steal secret informa
tion from it. Among the most prominent modelling techniques for security-c
ritical systems are attack trees. To overcome the lack of expressiveness r
egarding situational conditions such as timing\, concurrent countermeasure
s of the defender\, success probabilities and resources (especially costs)
\, several extensions of attack trees have been studied recently.\n\nIn th
is talk\, I introduce Attack-Defence Diagrams as an extension of attack tr
ees\, which can represent all of the aforementioned situational conditions
at the same time. Hence\, Attack-Defence Diagrams serve as an overarching
notation with respect to other existing extensions. In addition\, they ar
e equipped with a compositional semantics in terms of stochastic timed aut
omata\, which can be efficiently analysed using standard model checking to
ols such as the Modest Toolset. As I demonstrate by a case study from the
domain of cyber-security\, the semantics enables an efficient what-if quan
titative evaluation to deliver cost and success estimates for fixed strate
gies. Finally\, I show that the semantics naturally corresponds to a game
where its players compete to turn the outcome of the game from undecided t
o successful attack or defence\, respectively. This game formalisation for
ms a natural basis for future work in the domain of game theory.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160830T071434Z
DTSTAMP:20160830T071434Z
LAST-MODIFIED:20160906T064347Z
DTSTART;TZID=Europe/Berlin:20160913T150000
DTEND;TZID=Europe/Berlin:20160913T160000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:4354-537DEF00-3-14D67460
SUMMARY:Anca Muscholl: Distributed synthesis for acyclic architectures
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20140522T123609Z
DTSTAMP:20140522T123609Z
LAST-MODIFIED:20140814T140441Z
DTSTART;TZID=Europe/Berlin:20140716T100000
DTEND;TZID=Europe/Berlin:20140716T110000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
SEQUENCE:3
LOCATION:TUM MI 02.07.014
DESCRIPTION:Synthesizing distributed systems from specifications is an attr
active\nobjective\, since distributed systems are notoriously difficult to
get\nright. Unfortunately\, there are very few known decidable frameworks
\nfor distributed synthesis. We study a framework for synthesis\nof open s
ystems that is based on rendez-vous communication and causal\nmemory. In p
articular\, causal memory implies that specifications can talk about\nwhen
a communication takes place\, but cannot limit information that is\ntrans
mitted during communication. This choice is both realistic and\navoids som
e pathological reasons for undecidability. We show\na decidability result
for Zielonka automata with acyclic communication graphs\nand local omega-r
egular specifications. This is joint work with I. Walukiewicz.
ATTACH:http://www.model.in.tum.de/~schulzef/2014-07-16-Anca-Musholl.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4363-56B09900-3F-33F0B6C0
SUMMARY:Dmitry Chistikov: Navigating one-counter automata: Directions in th
e mountains
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160202T115603Z
DTSTAMP:20160202T115603Z
LAST-MODIFIED:20160219T111934Z
DTSTART;TZID=Europe/Berlin:20160226T100000
DTEND;TZID=Europe/Berlin:20160226T110000
TRANSP:OPAQUE
LOCATION:TUM MI 02.07.014
DESCRIPTION:One-counter automata (OCA) are finite-state automata with a cou
nter that supports increments\, decrements\, and tests for zero. They corr
espond to an intermediate class between regular and context-free languages
and are suitable for modeling ``counting'' phenomena. However\, reasoning
about OCA is often intractable: for example\, language equivalence is und
ecidable for nondeterministic OCA\, and for deterministic OCA it took 40 y
ears to prove the existence of short distinguishing words.\n\nIn this talk
\, I will give a review of reasoning tasks for OCA and discuss new tractab
ility results: (1) shortest paths between configurations of OCA are of at
most quadratic length\; (2) the Parikh image and sub-/superword closures o
f the language are accepted by small nondeterministic finite automata.\n\n
Based on work in FoSSaCS'16 (to appear) and under review.
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:4609-5760FA00-1-4CB93D00
SUMMARY:Martin Hofmann: A quantitative model of the simply-typed lambda cal
culus
LOCATION:LMU H1 1311
DESCRIPTION:Consider the simply-typed lambda calculus over one base type o
interpreted as the natural numbers. Suppose that the only constant is the
successor function S:o->o. Then\, if M is a closed term of type o->o its d
enotation is a function f:N->N such that f(x)<=x+c with c a constant. If\,
in addition\, M is allowed to contain a constant +:o->o->o representing
addition then its denotation will satisfy f(x)<=cx+d for constants c and d
. In both cases the constant(s) can be bounded by a tower of exponentials
of height the order of the types occurring in the term M.\n\nThis is not h
ard to see by considering a normal form of the term M but here we will giv
e a reduction-free proof using a non-standard quantitative semantics of th
e lambda calculus. The motivation of this problem comes from higher-order
model checking\; we hope that the quantitative semantics might eventually
be of use in that context.\n\nThis is joint work in progress with Jeremy L
edent and Igor Walukiewicz.\n
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160615T064908Z
DTSTAMP:20160615T064908Z
LAST-MODIFIED:20160615T064908Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20160617T090000
DTEND;TZID=Europe/Berlin:20160617T100000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:469F-5644C000-D-6DA33580
SUMMARY:Christian Kern: The Embedded Multicore Building Blocks Library and
its Verification
LOCATION:TUM MI 02.07.014
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20151112T163633Z
DTSTAMP:20151112T163633Z
LAST-MODIFIED:20151208T092003Z
DTSTART;TZID=Europe/Berlin:20151218T100000
DTEND;TZID=Europe/Berlin:20151218T110000
TRANSP:OPAQUE
DESCRIPTION:In this talk\, I will present the Embedded Multicore Building B
locks (EMB²\, https://github.com/siemens/embb)\, an easy to use yet powerf
ul and efficient C/C++ open source library for the development of parallel
applications. EMB² has been specifically designed for embedded systems an
d the typical requirements that accompany them\, such as real-time capabil
ity and constraints on memory consumption. As a major advantage\, low-leve
l operations are hidden in the library which relieves software developers
from the burden of thread management and synchronization. EMB² is independ
ent of the hardware architecture (x86\, ARM\, ...) and runs on various pla
tforms\, from small devices to large systems containing numerous processor
cores.\n\nDue to the non-deterministic nature of concurrent algorithms\,
bugs may occur sporadically\, so testing is an inadequate measure for veri
fying correctness. We therefore apply more sufficient verification methods
to EMB²\, like exhaustive scheduling and model checking. In two master th
eses we verify complex concurrent algorithms with different verification t
ools: Microsoft Chess\, Divine\, Maple and Fast Linearizability Checker. I
will report on the results and experiences gained by applying these tools
.
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:48D1-54D09900-39-4C043400
SUMMARY:Andrei Popescu: Consistency of the logic of Isabelle/HOL
LOCATION:TUM MI 01.09.014
DESCRIPTION:Gordon's Higher-Order Logic (HOL) extends Church's HOL with ran
k-1 polymorphism and a mechanism for non-empty type definitions carved out
of existing types. In turn\, the logic of Isabelle/HOL is an extension of
Gordon's logic with a more flexible mechanism for constant definitions: a
constant can be *declared*\, and later in the development\, possibly afte
r other type and constant definitions\, one or more instances of it can be
*defined*. (This is a distinguishing feature of Isabelle/HOL among the o
ther HOL-based provers\, and forms the basis of Isabelle/HOL's Haskell-sty
le type classes.)\n\nIt is widely believed that checking termination of th
e introduced dependencies from type and constant-instance definitions ensu
res consistency. However\, a purely syntactic rewriting argument for this
is hard to make due to the subtle dependencies through type definitions an
d the requirement that new types be provably non-empty. We give a simple p
roof of consistency based on revisiting and adjusting HOL's set-theoretic
semantics.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150203T094710Z
DTSTAMP:20150203T094710Z
LAST-MODIFIED:20150203T094946Z
DTSTART;TZID=Europe/Berlin:20150216T101500
DTEND;TZID=Europe/Berlin:20150216T110000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:49BD-55671800-1-514A8A80
SUMMARY:Ratul Saha: Distributed Markov Chains
LOCATION:LMU D Z007
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150528T133008Z
DTSTAMP:20150528T133008Z
LAST-MODIFIED:20150626T124310Z
DTSTART;TZID=Europe/Berlin:20150626T083000
DTEND;TZID=Europe/Berlin:20150626T093000
TRANSP:OPAQUE
DESCRIPTION:The formal verification of large probabilistic models is challe
nging. Exploiting the concurrency that is often present is one way to addr
ess this problem. Here we study a class of communicating probabilistic age
nts in which the synchronizations determine the probability distribution f
or the next moves of the participating agents. The key property of this cl
ass is that the synchronizations are deterministic\, in the sense that any
two simultaneously enabled synchronizations involve disjoint sets of agen
ts. As a result\, such a network of agents can be viewed as a succinct and
distributed presentation of a large global Markov chain. A rich class of
Markov chains can be represented this way. We use partial-order notions to
define an interleaved semantics that can be used to efficiently verify pr
operties of the global Markov chain represented by the network. To demonst
rate this\, we develop a statistical model checking (SMC) procedure and us
e it to verify two large networks of probabilistic agents. In this talk we
will give a brief overview of the model and the verification techniques\,
and discuss at length about potential advancements and application domain
s.
ATTACH:https://www7.in.tum.de/~schulzef/2015-06-26-Ratul-Saha.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:49CD-5379A580-3-679AE180
SUMMARY:Coinduction\, Equilibrium and Rationality of Escalation Pierre Lesc
anne\, ENS Lyon
LOCATION:TUM Garching - Room 01.11.018
DESCRIPTION:Escalation is the behavior of players who play forever in the s
ame\ngame. Such a situation is a typical field for application of\ncoindu
ction which is the tool conceived for reasoning in infinite\nmathematical
structures. In particular\, we use coinduction to study\nformally the game
called --dollar auction--\, which is considered as\nthe paradigm of escal
ation. Unlike what is admitted since 1971\, we\nshow that\, provided one
assumes that the other agent will always stop\,\nbidding is rational\, bec
ause it results in a subgame perfect\nequilibrium. We show that this is n
ot the only rational strategy\nprofile (the only subgame perfect equilibri
um). Indeed if an agent\nstops and will stop at every step\, whereas the
other agent keeps\nbidding\, we claim that he is rational as well because
this corresponds\nto another subgame perfect equilibrium. In the infinite
dollar\nauction game the behavior in which both agents stop at each step
is\nnot a Nash equilibrium\, hence is not a subgame perfect equilibrium\,\
nhence is not rational. Fortunately\, the notion of rationality based\non
coinduction fits with common sense and experience. Finally the\npossibil
ity of a rational escalation in an arbitrary game can be\nexpressed as a p
redicate on games and the rationality of escalation in\nthe dollar auction
game can be proved as a theorem which we have\nverified in the proof assi
stant COQ. In this talk we will recall the\nprinciples of infinite extens
ive games and use them to introduce\ncoinduction and equilibria (Nash equi
librium\, subgame perfect\nequilibrium). We will show how one can prove t
hat the two strategy\nprofiles presented above are equilibria and how this
leads to a\nrational escalation in the dollar auction. We will show that
\nescalation may even happen in much simpler game named 0\,1-game.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:beyene@in.tum.de
CREATED:20140519T063404Z
DTSTAMP:20140519T063404Z
LAST-MODIFIED:20140528T105842Z
DTSTART;TZID=Europe/Berlin:20140526T170000
DTEND;TZID=Europe/Berlin:20140526T180000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
ATTACH:http://www.model.in.tum.de/~schulzef/2014-05-26-Lescanne.pdf
BEGIN:VALARM
TRIGGER;RELATED=START;VALUE=DURATION:-P3D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4C54-5656F180-B-1BB76260
SUMMARY:Jerome Leroux: Witnesses for Vector Addition Systems
LOCATION:TUM MI 02.07.014
CLASS:PUBLIC
CREATED:20151126T114707Z
DTSTAMP:20151126T114707Z
LAST-MODIFIED:20151222T114425Z
DTSTART;TZID=Europe/Berlin:20151221T160000
DTEND;TZID=Europe/Berlin:20151221T170000
TRANSP:OPAQUE
DESCRIPTION:Vector addition systems or equivalently Petri nets are one of t
he most popular formal models for the representation and the analysis of p
arallel processes. Many known problems for vector addition systems are sho
wn to be decidable thanks to the theory of well-structured transition syst
ems. Indeed\, vector addition systems with configurations equipped with th
e classical point-wise ordering are well-structured transition systems. Ba
sed on this observation\, problems like the coverability or the terminatio
n are shown to be decidable. However\, the well-structured transition syst
ems theory cannot explain the decidability of the reachability problem. In
this presentation\, we show that runs of vector addition systems can be e
quipped with a well quasi-order that satisfies an amalgamation property. T
his observation provides a unifying way for solving many problems for vect
or addition systems including the central reachability problem.
SEQUENCE:1
ATTACH:https://www7.in.tum.de/~schulzef/2015-12-21-Jerome-Leroux.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4CEE-570CE300-9-42EBEA00
SUMMARY:Sander Leemans: Process mining in practice and theory
LOCATION:TUM MI 02.07.014
DESCRIPTION:Business processes are everywhere: from calling a bank to buyin
g an air ticket\, applying for a mortgage and sending a Whatsapp message.
Most processes are supported by information systems\, which typically log
everything that happens. Process mining aims to extract information from t
his data. First step is to discover a process model: a detailed descriptio
n what steps can be executed for a customer. This process model can then b
e used to identify and understand bottlenecks\, inefficient parts\, deviat
ions and risks. Process mining enables organisations to discover and impro
ve their processes as they really happen.\n\nIn this talk\, Sander will gi
ve a brief overview of process mining and dive a bit deeper into the first
step: discovering a control-flow model.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160412T115936Z
DTSTAMP:20160412T115936Z
LAST-MODIFIED:20160513T065441Z
DTSTART;TZID=Europe/Berlin:20160420T150000
DTEND;TZID=Europe/Berlin:20160420T160000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2016-04-20-Sander-Leemans.pptx
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4CEE-570CF280-1F-42EBEA00
SUMMARY:Reza Sefidgar: Formalizing the Ford-Fulkerson algorithm using Isabe
lle/HOL
LOCATION:TUM MI 02.07.014
DESCRIPTION:The Ford-Fulkerson algorithm is a method for solving the Maximu
m-Flow-Problem in networks. I will introduce the idea of the algorithm and
the abstractions that Iused to model this problem in Isabelle. I also ske
tch the correctness proof of the Ford-Fulkerson algorithm\, and present th
e Ford-Fulkerson theorem in Isablle. In my thesis I developed a verified i
mplementation of the algorithm using refinement techniques. I will overvie
w the steps which were applied during refinement and present the evaluatio
n of the final code in Standard ML.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160412T130546Z
DTSTAMP:20160412T130546Z
LAST-MODIFIED:20160412T130731Z
DTSTART;TZID=Europe/Berlin:20160414T160000
DTEND;TZID=Europe/Berlin:20160414T170000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:4D56-55004B00-41-56F09000
SUMMARY:Alexander Weinert: Automatically Proving Memory Safety and Terminat
ion of C-Programs
LOCATION:TUM MI 02.07.014
DESCRIPTION:Even though proving termination of a given program is undecidab
le in general\, several approaches have been developed to show termination
of large classes of programs.\nOf special interest is the analysis of rea
l-world languages\, such as C\, which feature runtime memory-allocation an
d explicit pointer-arithmetic.\n\nIn this talk\, we present a method for s
howing termination of C-programs.\nFor this\, we first introduce Symbolic
Execution Graphs\, which represent an overapproximation of all runs of the
program and can be used to show that it is memory safe.\nWe subsequently
transform these graphs into Integer Transition Systems\, whose termination
implies termination of the program.\n\nThis technique has been implemente
d in the tool AProVE at RWTH Aachen University.\nWe also compare its resul
ts with those of other verification tools that show termination of C-progr
ams.
CLASS:PUBLIC
CREATED:20150311T140227Z
DTSTAMP:20150311T140227Z
LAST-MODIFIED:20150311T140237Z
DTSTART;TZID=Europe/Berlin:20150313T100000
DTEND;TZID=Europe/Berlin:20150313T110000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4F0F-586C9B00-19-5FF4C600
SUMMARY:Sergiy Bogomolov: Scalable Static Hybridization Methods for Analysi
s of Nonlinear Systems
LOCATION:tba
DESCRIPTION:Hybridization methods enable the analysis of hybrid automata wi
th complex\, nonlinear dynamics through a sound abstraction process. Compl
ex dynamics are converted to simpler ones with added noise\, and then anal
ysis is done using a reachability method for the simpler dynamics. Several
such recent approaches advocate that only “dynamic” hybridization techniq
ues—i.e.\, those where the dynamics are abstracted on-the-fly during a rea
chability computation— are effective. In this talk\, we demonstrate this i
s not the case\, and create static hybridization methods that are more sca
lable than earlier approaches.\n\nThe main insight in our approach is that
quick\, numeric simulations can be used to guide the process\, eliminatin
g the need for an exponential number of hybridization domains. Transitions
between domains are generally time-triggered\, avoiding accumulated error
from geometric intersections. We enhance our static technique by combinin
g time-triggered transitions with occasional space-triggered transitions\,
and demonstrate the benefits of the combined approach in what we call mix
ed-triggered hybridization. Finally\, error modes are inserted to confirm
that the reachable states stay within the hybridized regions.\n\nThe devel
oped techniques can scale to higher dimensions than previous static approa
ches\, while enabling the parallelization of the main performance bottlene
ck for many dynamic hybridization approaches: the nonlinear optimization r
equired for sound dynamics abstraction. We implement our method as a model
transformation pass in the HYST tool\, and perform reachability analysis
and evaluation using an unmodified version of SpaceEx on nonlinear models
with up to six dimensions\n\nBio:\n\nSergiy Bogomolov is a Lecturer (Assi
stant Professor) at the Australian National University. Prior to joining A
NU Sergiy was a Postdoctoral Researcher in the Institute of Science and Te
chnology Austria. Sergiy is interested in verification and synthesis techn
iques for cyber-physical systems and their applications in artificial inte
lligence and systems biology. His Ph.D. and M.Sc. degrees are from the Uni
versity of Freiburg\, Germany.
CLASS:PUBLIC
CREATED:20170104T064959Z
DTSTAMP:20170104T064959Z
LAST-MODIFIED:20170104T065019Z
DTSTART;TZID=Europe/Berlin:20170109T150000
DTEND;TZID=Europe/Berlin:20170109T160000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:4FF2-53C7AA80-1-62F76880
SUMMARY:PUMA talk by Annette Bieniusa
LOCATION:TUM MI 02.07.014
DESCRIPTION:tba
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:beyene@in.tum.de
CREATED:20140717T105154Z
DTSTAMP:20140717T105154Z
LAST-MODIFIED:20140717T105154Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20141010T083000
DTEND;TZID=Europe/Berlin:20141010T093000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
END:VEVENT
BEGIN:VEVENT
UID:50A5-5704C100-1-48CEC380
SUMMARY:André Platzer: Logic of Hybrid Games
LOCATION:TUM MI 02.07.014
DESCRIPTION:Hybrid systems model cyber-physical systems as dynamical system
s with interacting discrete transitions and continuous evolutions along di
fferential equations. They arise frequently in many application domains\,
including aviation\, automotive\, railway\, and robotics. This talk studie
s hybrid games\, i.e. games on hybrid systems combining discrete and conti
nuous dynamics. Unlike hybrid systems\, hybrid games allow choices in the
system dynamics to be resolved adversarially by different players with dif
ferent objectives.\n\nThis talk describes how logic and formal verificatio
n can be lifted to hybrid games. The talk describes a logic for hybrid sys
tems called differential game logic dGL. The logic dGL can be used to stud
y the existence of winning strategies for hybrid games\, i.e. ways of reso
lving the player's choices in some way so that he wins by achieving his ob
jective for all choices of the opponent. Hybrid games are determined\, i.e
. one player has a winning strategy from each state\, yet their winning re
gions may require transfinite closure ordinals. The logic dGL\, neverthele
ss\, has a sound and complete axiomatization relative to any expressive lo
gic. Separating axioms are identified that distinguish hybrid games from
hybrid systems. Finally\, dGL is proved to be strictly more expressive tha
n the corresponding logic of hybrid systems.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160406T075709Z
DTSTAMP:20160406T075709Z
LAST-MODIFIED:20160411T065329Z
DTSTART;TZID=Europe/Berlin:20160414T140000
DTEND;TZID=Europe/Berlin:20160414T150000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:52C1-535FA400-13-77879C0
SUMMARY:Interprocedural Analysis of Hyper-Safety Properties
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20140429T130921Z
DTSTAMP:20140429T130921Z
LAST-MODIFIED:20140429T140357Z
DTSTART;TZID=Europe/Berlin:20140425T083000
DTEND;TZID=Europe/Berlin:20140425T093000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
ATTACH:http://www7.in.tum.de/~schulzef/2014-04-25-Seidl.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:5519-559BA900-7-70865D00
SUMMARY:Zuzana Komarkova: Unified View on Multiple Mean-Payoff Objectives i
n Markov Decision Processes
LOCATION:tba
DESCRIPTION:We investigate Markov decision processes (MDPs) with multiple l
ong-run average (also called mean-payoff) objectives. There exist two diff
erent views on the topic: (i) the expectation semantics\, where the goal i
s to optimize the expected mean-payoff value\, and (ii) the satisfaction s
emantics\, where the goal is to maximize the probability of runs such that
the mean-payoff value stays above a given vector. We consider optimizatio
n problem with respect to both views at once\, thus unifying the existing
semantics. Our goal is to optimize the expectation while ensuring the sati
sfaction constraint. This problem captures the notion of optimization wit
h respect to strategies that are risk-averse (i.e.\, ensure certain probab
ilistic guarantee). We present algorithms for the respective decision prob
lems as well as for Pareto curve approximation\, which are all polynomial
in the size of the MDP. We also present a complete characterization of the
strategy complexity (in terms of memory bounds and randomization) require
d to solve our problem. The solution is based on a co-authorial article Un
ifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Pro
cesses\, to appear in the conference Logic in Computer Science (LICS)\, an
d author's own results.
CLASS:PUBLIC
CREATED:20150707T102433Z
DTSTAMP:20150707T102433Z
LAST-MODIFIED:20150707T102444Z
DTSTART;TZID=Europe/Berlin:20150731T080000
DTEND;TZID=Europe/Berlin:20150731T090000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:557A-559BA780-7-73662680
SUMMARY:Jens Oehlerking: Specification Models for Cyber-Physical Systems in
Industrial Practice
LOCATION:TUM MI 01.07.023
DESCRIPTION:ABSTRACT:\nThis talk will focus on the challenges in modeling a
nd verification that need to be overcome to ensure the applicability of re
search results in industrial practice. A particular focus will be on the
specification of verification conditions\, with real life examples that il
lustrate the limits of differentmodeling formalisms that were encountered
in practice. Based on several representative classes of specifications\, t
his talk will discuss at how they can be modeled and how the resulting mod
el scan be leveraged for verification and testing. The modeling formalisms
considered in this talk include temporal logics\, signal metrics and hybr
id automata. Different verification and testing approaches that are of imp
ortance in practice are also discussed.\n\nBIO:\nJens Oehlerking completed
his PhD in 2011 at the University of Oldenburg on the subject of verifica
tion techniques for stability properties of hybrid systems. Afterwards\, h
e joined the Corporate Research of Robert Bosch GmbH\, where he is current
ly working as a research engineer in the Software Systems department on to
pics of modeling\, testing\, structuring\, and verification of cyber-physi
cal systems. The main focus of his work is the transfer of results from th
e academic communities in the area of formal methods into industrial pract
ice. His current research interests include the application of formal meth
ods to automated driving and other real life examples\, requirements speci
fication\, model-based testing and novel modeling paradigms for cyber-phys
ical systems.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150707T102138Z
DTSTAMP:20150707T102138Z
LAST-MODIFIED:20150707T102138Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20150714T140000
DTEND;TZID=Europe/Berlin:20150714T150000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:5681-591D5E80-71-5DF3D180
SUMMARY:Javier Esparza: Static Analysis of Deterministic Negotiations
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170518T084222Z
DTSTAMP:20170518T084222Z
LAST-MODIFIED:20170619T102722Z
DTSTART;TZID=Europe/Berlin:20170623T083000
DTEND;TZID=Europe/Berlin:20170623T093000
TRANSP:OPAQUE
SEQUENCE:2
LOCATION:LMU D Z005
DESCRIPTION:Negotiation diagrams are a model of concurrent computation akin
to workflow Petri nets. Deterministic negotiation diagrams are essential
ly equivalent to free-choice workflow Petri nets\, but with a built-in par
tition of the workflow. Deterministic negotiations are surprisingly amenab
le to verification. Soundness and several other fundamental questions can
be decided in PTIME for sound deterministic negotiation diagrams\, while t
hey are PSPACE-hard in the general case.\n\nIn this paper we generalize an
d explain these results. We introduce a general static analysis framework
for negotiations\, and define Mazurkiewicz-invariant static analysis probl
ems\, which encompass the questions above and new ones.\n\nWe show that Ma
zurkiewicz-invariant analysis problems can be solved in PTIME for sound de
terministic negotiations iff they can be solved in PTIME for sequential fl
ow-graphs---even though the flow-graph of a deterministic negotiation diag
ram can be exponentially larger than the diagram itself.\n\nOur result is
based on a novel decomposition theorem\, of independent interest\, showing
that sound deterministic negotiation diagrams can be hierarchically decom
posed into (possibly overlapping) smaller sound diagrams.
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:5715-58763800-4D-28871240
SUMMARY:Dmitry Zaitsev: Universal Petri and Sleptsov Nets
LOCATION:TUM MI 00.09.038
DESCRIPTION:A universal Petri net (UPN) represents a processor in the Petri
net paradigm of computing [5].\nA UPN executes (runs) a program specified
by a Petri net (PN) which initial marking represents\ninput data and fina
l marking represents output data.\nA crucial obstacle for application of P
etri nets as a general-purpose language for concurrent\nprogramming [5] co
nsists in the fact they run exponentially slower comparing Turing machines
.\nA class of place/transition nets with multiple firing of a transition a
t a step has been called\nSleptsov nets. Sleptsov nets run fast compared t
o Petri nets [4] that opens prospects for their\npractical application [3]
and composition of efficient universal Sleptsov nets (USNs) [1].\nA serie
s of UPNs/USNs have been constructed in an explicit form via: a) direct sp
ecification of\nthe state equation of an inhibitor PN [8]\; b) simulation
of small universal Turing machines by a\ndeterministic inhibitor PN [6]\;
c) simulation of an elementary cellular automata Rule 110 by\ninfinite (co
nventional) PNs [2]\; d) direct specification of Markov normal algorithm r
ules by an\ninhibitor PN [8]\; e) simulation of small universal Turing mac
hines by a deterministic inhibitor\nSleptsov net [1]. An encoded PN/SN is
loaded into dedicated places of a UPN/USN. Small\nuniversal Turing machine
s and universal cellular automata employ sophisticated chains of\nencoding
s (simulations). Obtained small universal nets contain less than half a hu
ndred nodes.\nWhen constructing universal nets\, a library of subnets has
been completed for computing basic\narithmetic\, logic\, and copying opera
tions. A technique for specification of a given algorithm by\na PN (SN) pr
ogram has been developed to combine data with control flows\, implement ba
sic\noperators of branching\, loop\, parallel execution\, and subroutine (
subnet) call-return. To\ncombine data with control flows\, special dashed
and dotted arcs have been introduced as\nabbreviations for composition of
copying subnets.\nAn advantage of the approach is its conceptual unity. On
ly PNs/SNs are applied for\nprogramming and running programs. High-level n
ets\, using modular principle of composition\n(subnets)\, are compiled int
o a plain low-level inhibitor/priority net which is considered as an\nanal
og to assembler language. Then a UPN/USN runs the obtained net.\nExamples
of RSA encryption/decryption\, solving Laplace equation\, and computing a
fuzzy\nlogic function accomplish the presentation of universal nets and il
lustrate principles of\nprogramming in Petri/Sleptsov nets.\n\nhttp://memb
er.acm.org/~daze\n\nBasic References\n1. Zaitsev D.A. Universal Sleptsov N
et\, International Journal of Computer Mathematics (to appear)\n2. Zaitsev
D.A. Simulating Cellular Automata by Infinite Petri Nets\, Journal of Cel
lular Automata (to appear)3. Zaitsev D.A.\, Jürjens J. Programming in the
Sleptsov Net Language for Systems Control\, Advances in Mechanical Enginee
ring\, 2016\, Vol. 8(4)\, 1–11.\n4. Zaitsev D.A. Sleptsov Nets Run Fast\,
IEEE Transactions on Systems\, Man\, and Cybernetics: Systems\, 2016\, Vol
. 46(5)\, 682–693.\n5. Zaitsev D.A. Paradigm of Computations on the Petri
Nets\, Automation and Remote Control\, 2014\, Vol. 75(8)\, 1369–1383.\n6.
Zaitsev D.A. Toward the Minimal Universal Petri Net\, IEEE Transactions on
Systems\, Man\, and Cybernetics: Systems\, 2014\, Vol. 44(1)\, 47–58.\n7.
Zaitsev D.A. Inhibitor Petri Net Executing an Arbitrary Given Markov Norm
al Algorithm\, Automatic Control and Computer Sciences\, 2012\, Vol. 46(7)
\, 345–355.\n8. Zaitsev D.A. Universal Petri net\, Cybernetics and Systems
Analysis\, 2012\, Vol. 48(4)\, 498–511.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170111T135240Z
DTSTAMP:20170111T135240Z
LAST-MODIFIED:20170130T143203Z
DTSTART;TZID=Europe/Berlin:20170127T100000
DTEND;TZID=Europe/Berlin:20170127T110000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2017-01-27-Dmitry-Zaitsev.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:58D8-574C1E00-3-3EE26D4
SUMMARY:Stefan Jaax: Limit-Deterministic Büchi Automata for Linear Temporal
Logic
CLASS:PUBLIC
CREATED:20160530T110333Z
DTSTAMP:20160530T110333Z
LAST-MODIFIED:20160603T130524Z
DTSTART;TZID=Europe/Berlin:20160610T090000
DTEND;TZID=Europe/Berlin:20160610T100000
TRANSP:OPAQUE
LOCATION:LMU H1 1311
DESCRIPTION:A Büchi automaton is said to be limit-deterministic if every s
tate reachable from an accepting state is deterministic. In this talk we a
re going to present a direct construction from an LTL formula to a limit-d
eterministic Büchi automaton. Contrary to the indirect approach of constru
cting a non-deterministic automaton for the input formula and then applyin
g a semi-determinisation algorithm\, our translation is compositional and
has a clear logical structure. It yields much smaller automata for formula
s with deep nesting of modal operators and performs at least as well as th
e existing approaches on general formulas. Moreover\, the resulting automa
ton can be directly applied to quantitative probabilistic model-checking\,
using standard techniques known for deterministic automata.
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:58EF-56A63B80-15-26BAD6C0
SUMMARY:Daniel Neider: Robust Linear Temporal Logic
LOCATION:TUM MI 02.07.014
DESCRIPTION:Although it is widely accepted that every system should be robu
st\, in the sense that ``small'' violations of environment assumptions sho
uld lead to ``small'' violations of system guarantees\, it is less clear h
ow to make this intuitive notion of robustness mathematically precise. In
this paper\, we address this problem by developing a robust version of the
Linear Temporal Logic (LTL) fragment that only contains the always and ev
entually temporal operators. We denote this new logic by rLTL$(\\boxdot\,\
\Diamonddot)$. Its formulas are syntactically identical to LTL formulas bu
t are endowed with a many-valued semantics that encodes robustness. In par
ticular\, the semantics of the rLTL formula $\\varphi\\Rightarrow \\psi$ i
s such that a ``small'' violation of the environment assumption $\\varphi$
is guaranteed to only produce a ``small'' violation of the system guarant
ee $\\psi$. In addition to introducing rLTL$(\\boxdot\,\\Diamonddot)$\, we
study the verification and synthesis problems for this logic: similar to
LTL\, we show that both problems are decidable\, that the verification pro
blem can be solved in time exponential in the number of subformulas of the
rLTL formula at hand\, and that the synthesis problem can be solved in do
ubly exponential time. All the results for rLTL$(\\boxdot\,\\Diamonddot)$
smoothly extend to full rLTL\, the robust version of full LTL.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160125T151340Z
DTSTAMP:20160125T151340Z
LAST-MODIFIED:20160125T151340Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20160129T140000
DTEND;TZID=Europe/Berlin:20160129T150000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:5AD-56404A80-31-675F9900
SUMMARY:Anca Muscholl: Word transducers: from 2-way to 1-way
LOCATION:TUM MI 02.07.014
DESCRIPTION:Two-way finite-state transducers on words are strictly more exp
ressive than one-way transducers. It has been shown recently how to decide
if a two-way functional transducer has an equivalent one-way transducer [
Gauwin et al 2013]\, and the complexity of the algorithm is non-elementary
. We propose an alternative and simpler algorithm for sweeping functional
transducers\, namely\, transducers that can only reverse their head direct
ion at the extremities of the input. Our algorithm works in doubly exponen
tial space and\, in the positive case\, produces an equivalent one-way tra
nsducer of doubly exponential size. We also show that the bound on the siz
e of the transducer is tight\, and that the one-way definability problem i
s undecidable for non-functional transducers.\n\n(joint work with F. Basch
enis\, O. Gauwin\, G. Puppis\, FSTTCS’15)
CLASS:PUBLIC
CREATED:20151109T072600Z
DTSTAMP:20151109T072600Z
LAST-MODIFIED:20151118T150157Z
DTSTART;TZID=Europe/Berlin:20151113T100000
DTEND;TZID=Europe/Berlin:20151113T110000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2015-11-13-Muscholl.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:5BEF-5A009800-B1-3FCFE6C0
SUMMARY:Florian Zuleger: Ranking Functions for Vector Addition Systems
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20171106T171328Z
DTSTAMP:20171106T171328Z
LAST-MODIFIED:20171120T201830Z
DTSTART;TZID=Europe/Berlin:20171124T100000
DTEND;TZID=Europe/Berlin:20171124T110000
TRANSP:OPAQUE
DESCRIPTION:Vector addition systems are an important model in theoretical c
omputer science and have been used for the analysis of systems in a variet
y of areas. Termination is a crucial property of vector addition systems a
nd has received considerable interest in the literature. In this talk we g
ive a complete method for the construction of ranking functions for vector
addition systems with states. The interest in ranking functions is motiva
ted by the fact that ranking functions provide valuable additional informa
tion in case of termination: They provide an explanation for the progress
of the vector addition system\, which can be reported to the user of a ver
ification tool\, and can be used as certificates for termination. Moreover
\, we show how ranking functions can be used for the computational complex
ity analysis of vector addition systems (here complexity refers to the num
ber of steps the vector addition system under analysis can take in terms o
f the given initial vector).
LOCATION:TUM MI 02.07.034
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:5C05-59CAB880-1-D498200
SUMMARY:Axel Legay: On Statistical Model Checking
LOCATION:TUM MI 03.09.14
DESCRIPTION:Model checking offers the possibility to automatically verify t
he correctness of complex systems or detect bugs. In many practical applic
ations it is also useful to quantify the probability of a property (e.g.\,
system failure)\, so the concept of model checking has been extended to p
robabilistic systems. This form is frequently referred to as numerical mod
el checking.\n\nTo give results with certainty\, numerical model checking
algorithms effectively perform an exhaustive traversal of the states of th
e system. In most real applications\, however\, the state space is intract
able\, scaling exponentially with the number of independent state variable
s (the state explosion problem). Abstraction and symmetry reduction may ma
ke certain classes of systems tractable\, but these techniques are not gen
erally applicable. This limitation has prompted the development of statist
ical model checking (SMC)\, which employs an executable model of the syste
m to estimate the probability of a property from simulations.\n\nSMC is a
Monte Carlo method which takes advantage of robust statistical techniques
to bound the error of the estimated result. To quantify a property it is n
ecessary to observe the property\, while increasing the number of observat
ions generally increases the confidence of the estimate. Rare properties a
re often highly relevant to system performance (e.g.\, bugs and system fai
lure are required to be rare) but pose a problem for statistical model che
cking because they are difficult to observe. Fortunately\, rare event tech
niques such as importance sampling and importance splitting may be success
fully applied to statistical model checking.\n\nImportance sampling and im
portance splitting have been widely applied to specific simulation problem
s in science and engineering. Importance sampling works by estimating a re
sult using weighted simulations and then compensating for the weights. Imp
ortance splitting works by reformulating the rare probability as a product
of less rare probabilities conditioned on levels that must be achieved.\n
\nIn this talk\, we will introduce Statistical Model Checking and summariz
e our contributions on importance splitting. Then\, we discuss their imple
mentation within the Plasma toolset.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170926T203337Z
DTSTAMP:20170926T203337Z
LAST-MODIFIED:20170926T203337Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20171004T140000
DTEND;TZID=Europe/Berlin:20171004T150000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:5CF4-55A78600-3-20EE678
SUMMARY:Sebastian Hack: AnyDSL: Building Domain-Specific Languages for Prod
uctivity and Performance
LOCATION:TUM MI 02.07.014
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150716T102332Z
DTSTAMP:20150716T102332Z
LAST-MODIFIED:20150716T102332Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20150720T100000
DTEND;TZID=Europe/Berlin:20150720T110000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:5EA2-54BF7D00-29-64BD4500
SUMMARY:Xavier Rival: Construction of modular abstract domains for heteroge
neous properties
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150121T101856Z
DTSTAMP:20150121T101856Z
LAST-MODIFIED:20150210T093302Z
DTSTART;TZID=Europe/Berlin:20150202T110000
DTEND;TZID=Europe/Berlin:20150202T120000
TRANSP:OPAQUE
LOCATION:TUM MI 02.07.014
SEQUENCE:1
DESCRIPTION:In this talk\, we study the construction of shape-numeric stati
c analysers\, and the combination of several memory abstractions in a sing
le shape analysis tool. We set up an abstract interpretation framework tha
t allows to reason about simultaneous shape-numeric properties by combinin
g shape and numeric abstractions into a modular\, expressive abstract doma
in. Such a modular structure is highly desirable to make its formalisatio
n\, proof and implementation easier to perform and to get correct. Further
more\, we extend this modular abstract domains so as to combine different
memory abstractions\, for better scalability and greater expressiveness. T
his framework is implemented in the MemCAD static analyser.
ATTACH:https://www7.in.tum.de/~schulzef/2015-02-02-Xavier-Rival.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:5EA2-54BF7D00-31-64BD4500
SUMMARY:David Pichardie: Formal Verification of a C Static Analyzer
LOCATION:TUM MI 02.07.014
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150121T101959Z
DTSTAMP:20150121T101959Z
LAST-MODIFIED:20150210T093332Z
DTSTART;TZID=Europe/Berlin:20150203T093000
DTEND;TZID=Europe/Berlin:20150203T103000
TRANSP:OPAQUE
DESCRIPTION:We report on the design and soundness proof\, using the Coq pro
of assistant\, of Verasco\, a static analyzer based on abstract interpreta
tion for most of the ISO C 1999 language (excluding recursion and dynamic
allocation)\, which establishes the absence of run-time errors in the anal
yzed programs. Verasco enjoys a modular architecture that supports the ext
ensible combination of multiple abstract domains\, both relational and non
-relational. Verasco integrates with the CompCert C formally-verified comp
iler so that not only the soundness of the analysis results is guaranteed
with mathematical certitude\, but also the fact that these guarantees carr
y over to the compiled executable code.
ATTACH:https://www7.in.tum.de/~schulzef/2015-02-03-David-Pichardie.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:6001-59009380-77-B99F1A0
SUMMARY:Christoph Haase: Presburger arithmetic and semi-linear sets: the pa
st\, the present and the future
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170426T123337Z
DTSTAMP:20170426T123337Z
LAST-MODIFIED:20170614T121909Z
DTSTART;TZID=Europe/Berlin:20170609T100000
DTEND;TZID=Europe/Berlin:20170609T110000
TRANSP:OPAQUE
LOCATION:TUM MI 02.13.010
DESCRIPTION:Presburger arithmetic\, the first-order theory of the natural n
umbers with addition and order\, is a fragment of number theory that was s
hown decidable in 1929 by Moj?esz Presburger in his Master's thesis. Seymo
ur Ginsburg and Edwin Spanier showed in 1966 that the sets definable in Pr
esburger arithmetic coincide with semi-linear sets\, a generalisation of u
ltimately periodic sets to higher dimensions. The goal of this talk is to
give a comprehensive overview about Presburger arithmetic and semi-linear
sets\, about their history and notable results. I will also discuss in mor
e detail some recent work on the descriptive complexity of Boolean operati
ons on semi-linear sets. This talk is partly based on joint work with Dmit
ry Chistikov.
SEQUENCE:1
ATTACH:https://www7.in.tum.de/~schulzef/2017-06-09-Christoph-Haase.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:6002-59109500-BF-38D68800
SUMMARY:Francesco Leofante: Are you doing what you think are doing? Robust
AI via verification\, monitoring and repair in robotics
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170508T155715Z
DTSTAMP:20170508T155715Z
LAST-MODIFIED:20170526T093359Z
DTSTART;TZID=Europe/Berlin:20170524T100000
DTEND;TZID=Europe/Berlin:20170524T110000
TRANSP:OPAQUE
LOCATION:TUM MI 02.07.014
DESCRIPTION:Abstract: Growing application areas for machine learning in rob
otics require \nthe exclusion or likely avoidance of unsafe behaviors. An
important question is then\, how confidence\nin system behaviors obtained
from machine learning can be improved by formal verification.\nIn this tal
k\, Francesco will overview some results obtained combining machine learni
ng techniques\n(e.g.\, Reinforcement Learning\, Support Vector Machines) a
nd formal verification (e.g.\, model checking\, SMT solving)\nto ensure sa
fety of (learning) robotic systems.\n\n\nBio: Francesco Leofante is a PhD
Student at the Theory of Hybrid Systems Group (RWTH Aaachen) and AIMSLab (
University of Genoa) under the supervision of\nProf. Erika Abraham and Pro
f. Armando Tacchella. Francesco received his MS Degree in Advanced Robotic
s from \nthe University of Genoa (2014) and from Ecole Centrale de Nantes
(2015). Previously\, he received a BS Degree in Electronics Engineering fr
om the University of Genoa (2013).
SEQUENCE:1
ATTACH:https://www7.in.tum.de/~schulzef/2017-05-24-Francesco-Leofante.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:6003-59109500-B9-66EEDC00
SUMMARY:Felix Klaedtke: Runtime Verification of Temporal Properties over Ou
t-of-order Streams
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170508T155534Z
DTSTAMP:20170508T155534Z
LAST-MODIFIED:20170704T150827Z
DTSTART;TZID=Europe/Berlin:20170630T083000
DTEND;TZID=Europe/Berlin:20170630T093000
TRANSP:OPAQUE
LOCATION:LMU D Z005
DESCRIPTION:In this talk\, I will describe a monitoring approach for verify
ing systems at runtime. The approach targets distributed systems whose co
mponents communicate with the monitors over unreliable channels. In parti
cular\, I will present the approach's underlying theory\, which is based o
n a new three-valued semantics for the real-time logic MTL. The three-valu
ed semantics is well suited to soundly and completely reason online about
event streams in the presence of message delay or loss. I will also sketch
its algorithmic realization for the propositional setting and its extensi
on to data values. Furthermore\, I will present initial experimental resu
lts\, obtained by our prototype implementation. When messages are receive
d out of order\, the prototype processes thousands of events per second in
a propositional setting and hundreds of events per second when accounting
for data values.\n\nThis is joint work with David Basin (ETH Zurich) and
Eugen Zalinescu (TU Munich).
SEQUENCE:1
ATTACH:https://www7.in.tum.de/~schulzef/2017-06-30-Felix-Klaedtke.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:6056-56E6AF80-33-50316700
SUMMARY:Lawrence Paulson: The First Mechanised Proof of the Second Incomple
teness Theorem
LOCATION:TUM MI 03.09.014
DESCRIPTION:Gödel’s incompleteness theorems are famous for what they assert
but also for the elaborate techniques used in the proofs. The first incom
pleteness theorem (asserting that all reasonable formalisations of arithme
tic leave some questions unresolved) involves coding the syntax of a forma
l system within its own logic to derive a contradiction. The second incomp
leteness theorem (asserting that no reasonable axiomatic system can prove
its own consistency) is variously proved through some sort of meta-argumen
t involving the first theorem\, or by using a more elaborate encoding\, an
d in either case relying on extended proofs within an extended formal calc
ulus. Three previous researchers formalised the first incompleteness theor
em without proceeding to the second. However\, the second theorem can be p
roved with a modest additional effort\, given the right techniques. The ta
lk will introduce the theorems and then outline the first ever formalised
proof of the second incompleteness theorem\, highlighting the key technica
l points.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160314T123432Z
DTSTAMP:20160314T123432Z
LAST-MODIFIED:20160411T111447Z
DTSTART;TZID=Europe/Berlin:20160408T100000
DTEND;TZID=Europe/Berlin:20160408T110000
TRANSP:OPAQUE
SEQUENCE:1
ATTACH:https://www7.in.tum.de/~schulzef/2016-04-08-Lawrence-Paulson.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:67D-56953180-B9-36076440
SUMMARY:Rüdiger Ehlers: Cooperative Reactive Synthesis
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160112T170249Z
DTSTAMP:20160112T170249Z
LAST-MODIFIED:20160309T062554Z
DTSTART;TZID=Europe/Berlin:20160129T100000
DTEND;TZID=Europe/Berlin:20160129T110000
TRANSP:OPAQUE
LOCATION:Raum 4981 (Stammgelände) https://portal.mytum.de/displayRoomMap?49
81@0509
SEQUENCE:2
DESCRIPTION:A modern approach to engineering correct-by-construction system
s is to synthesize them automatically from formal specifications. Oftentim
es\, a system can only satisfy its guarantees if certain environment assum
ptions hold\, which motivates their inclusion in the system specification.
Experience with modern synthesis approaches shows that synthesized system
s tend to satisfy their specifications by actively working towards the vio
lation of the assumptions rather than satisfying assumptions and guarantee
s together. Such uncooperative behavior is undesirable because it violates
the aim of synthesis: the system should try to satisfy its guarantees and
use the assumptions only when needed. Also\, the assumptions often descri
be the valid behavior of other components in a bigger system\, which shoul
d not be obstructed unnecessarily.\n\nWe present a hierarchy of cooperatio
n levels between system and environment. Each level describes how well the
system enforces both the assumptions and guarantees. We show how to synth
esize systems that achieve the highest possible cooperation level for a gi
ven specification in Linear Temporal Logic (LTL). The synthesized systems
can also exploit cooperative environment behavior during operation to reac
h a higher cooperation level that is not enforceable by the system initial
ly. The worst-case time complexity of our synthesis procedure is doubly-ex
ponential\, which matches the complexity of standard LTL synthesis. For on
e particularly interesting level of the hierarchy\, we also present a spec
ialized cooperative synthesis algorithm for generalized reactivity(1) spec
ifications that is complexity-theoretically optimal.\n\nThis talk is based
on joint work with Robert Könighofer and Roderick Bloem.
ATTACH:https://www7.in.tum.de/~schulzef/2016-01-29-Ruediger-Ehlers.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:67E-5693CA80-75-2389BFC0
SUMMARY:Anca Muscholl: On the verification of parametrized\, asynchronous s
ystems with shared memory
LOCATION:TUM MI 02.07.014
DESCRIPTION:Verification of concurrent systems is a difficult problem in ge
neral\, and this is even more the case in a parametrized setting where unb
oundedly many concurrent components are considered. Recently\, Hague and E
sparza et al. considered an architecture with a leader process and unbound
edly many copies of a contributor process interacting over a shared memory
. All processes in their setting are pushdown automata. Here\, we extend t
he framework and give general language-theoretical conditions on the class
es of transition systems for leader and contributors for which safety is a
decidable problem. We also discuss some questions beyond safety. (Joint w
ork with S. LaTorre\, I. Walukiewicz and M. Fortin.)\n
CLASS:PUBLIC
CREATED:20160111T153046Z
DTSTAMP:20160111T153046Z
LAST-MODIFIED:20160115T110224Z
DTSTART;TZID=Europe/Berlin:20160112T150000
DTEND;TZID=Europe/Berlin:20160112T160000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2016-01-12-Anca-Muscholl.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:6942-5593C480-4D-6AEF2100
SUMMARY:Aymeric Bouzy: Nonprimitive Corecursion in Isabelle/HOL
LOCATION:TUM MI 00.09.038
DESCRIPTION:Codatatypes can be used to model possibly infinite data. They h
ave been introduced in Isabelle/HOL in 2013. Since 2014\, there has been a
“primcorec” command as well\, for defining primitively corecursive functi
ons. We implement a foundational framework for corecursion support\, corec
\, that offers a lot more syntactic flexibility. In particular\, it allows
corecursion under friendly operations. The command corec results in much
shorter\, more natural definitions: for example\, the part of Traytel’s Co
inductive_Languages entry in the Archive of Formal Proofs that defines reg
ular operations can be shrunk to 12% of its size\, without the need to int
roduce intermediate constants\, and without writing a single proof line.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150701T104500Z
DTSTAMP:20150701T104500Z
LAST-MODIFIED:20150701T104500Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20150716T140000
DTEND;TZID=Europe/Berlin:20150716T150000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:6B8C-589B5080-15-3FE55A00
SUMMARY:Sebastian Söntges: Feasibility Analysis of Trajectory Planning Prob
lems of Automated Vehicles in Time-Varying Environments
LOCATION:TUM MI 00.09.038
DESCRIPTION:Trajectory planning for automated vehicles is a major problem i
n\nrobotics. This problem is in particular challenging for time-varying\ne
nvironments and systems with constraint dynamics. Commonly used\nsampling-
based planning algorithms are not complete in the sense\, that\nthey canno
t report in finite time infeasibility of the planning problem\,\ni.e. the
nonexistence of any solution. They rely on a discretization of\nthe contin
uous space of trajectories by deterministic or probabilistic\nsampling. Th
ereby\, they discover only a subset of the set of all possible\ntrajectori
es and may show feasibility of the planning problem\, but fail\nto detect
infeasible problems. In this work\, I present a method\, which\ncan prove
infeasibility for a class of relevant trajectory planning\nproblems of two
-dimensional motion with bounded speed and acceleration\nin time-varying e
nvironments. The proposed method computes an\nover-approximative represent
ation of the set of all reachable states of\nthe system at discrete points
in time. Thus\,it can formally guarantee\,\nthat no feasible trajectory e
xists if the computed reachable set becomes\nempty at some point in time.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170208T171040Z
DTSTAMP:20170208T171040Z
LAST-MODIFIED:20170315T090520Z
DTSTART;TZID=Europe/Berlin:20170210T100000
DTEND;TZID=Europe/Berlin:20170210T110000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2017-02-10-Sebastian-Soentges.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:6F5B-58AC0E00-3F-62704200
SUMMARY:Edon Kelmendi: Half-positional Two-player Stochastic Games
LOCATION:TUM MI 00.09.038
DESCRIPTION:We consider zero-sum stochastic games with perfect information
and finitely many states and actions. The payoff is computed by a function
which associates to each infinite sequence of states and actions a real n
umber. We prove that if the the payoff function is both shift-invariant an
d submixing\, then the game is half-positional\, i.e. the first player has
an optimal strategy which is both deterministic and stationary.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170221T095340Z
DTSTAMP:20170221T095340Z
LAST-MODIFIED:20170221T095340Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20170303T100000
DTEND;TZID=Europe/Berlin:20170303T110000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:71DE-55658D00-FB-2733A980
SUMMARY:Matthias Rungger: Feedback Refinement Relations for the Synthesis o
f Symbolic Controllers
LOCATION:LMU D Z007
DESCRIPTION:We present an abstraction and refinement methodology for the au
tomated controller synthesis to enforce general predefined specifications.
The designed controllers require quantized (or symbolic) state informatio
n only and can be interfaced with the system via a static quantizer. Both
features are particularly important with regard to any practical implement
ation of the designed controller and\, as we prove\, are characterized by
the existence of a feedback refinement relation between plant and abstract
ion. Feedback refinement relations are a novel concept of system relations
introduced in this paper. Our work builds on a general notion of system w
ith set-valued dynamics and possibly non-deterministic quantizers to permi
t the synthesis of controllers that robustly\, and provably\, enforce the
specification in the presence of various types of uncertainties and distur
bances. We identify a class of abstractions that is canonical in a well-de
fined sense\, and provide a method to efficiently compute canonical abstra
ctions of perturbed nonlinear sampled systems. We demonstrate the practica
lity of our approach on two examples -- a path planning problem for a mobi
le robot and an aircraft landing maneuver.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150527T092409Z
DTSTAMP:20150527T092409Z
LAST-MODIFIED:20150622T074104Z
DTSTART;TZID=Europe/Berlin:20150619T083000
DTEND;TZID=Europe/Berlin:20150619T093000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2015-06-19-Matthias-Rungger.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:734B-53620200-7-20354300
SUMMARY:On Refinements of Boolean and Parametric Modal Transition Systems
LOCATION:LMU E210
DESCRIPTION:We consider the extensions of modal transition systems (MTS)\,
namely\nBoolean MTS and parametric MTS and we investigate the refinement\n
problems over both classes. Firstly\, we reduce the problem of modal\nrefi
nement over both classes to a problem solvable by a QBF solver and\nprovid
e experimental results showing our technique scales well.\nSecondly\, we e
xtend the algorithm for thorough refinement of MTS\nproviding better compl
exity then via reductions to previously studied\nproblems. Finally\, we in
vestigate the relationship between modal and\nthorough refinement on the t
wo classes and show how the thorough\nrefinement can be approximated by th
e modal refinement.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20140501T081321Z
DTSTAMP:20140501T081321Z
LAST-MODIFIED:20140501T081451Z
DTSTART;TZID=Europe/Berlin:20140502T083000
DTEND;TZID=Europe/Berlin:20140502T093000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:7396-55794700-FB-38C97200
SUMMARY:Nathanaël Fijalkow: Trading Bounds for Memory in Games with Counter
s
LOCATION:TUM MI 02.07.014
DESCRIPTION:We study two-player games with counters played on graphs. We in
vestigate a conjecture by Colcombet and Löding which states the existence
of a trade-off between the size of the memory and the bound achieved on th
e counters. They proved that this conjecture implies the decidability of c
ost monadic second-order logic over infinite trees\, as well as the decida
bility of the Rabin-Mostowski parity index.\n\nWe show that unfortunately
the conjecture does not hold: there is no trade-off between bounds and mem
ory\, even for finite arenas. On the positive side\, we prove the existenc
e of a trade-off for the special case of thin tree arenas. This allows to
extend the theory of regular cost functions over thin trees\, and obtain a
s a corollary the decidability of cost monadic second-order logic over thi
n trees.\n\nThis is a joint work with Florian Horn\, Denis Kuperberg and M
icha? Skrzypczak\, which will be presented at ICALP'2015.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150611T083029Z
DTSTAMP:20150611T083029Z
LAST-MODIFIED:20150615T141012Z
DTSTART;TZID=Europe/Berlin:20150618T160000
DTEND;TZID=Europe/Berlin:20150618T170000
TRANSP:OPAQUE
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:7471-53A14200-1-12DA95C0
SUMMARY:When the decreasing sequence fails by Nicolas Halbwachs
LOCATION:Garching - FMI 02.07.014
DESCRIPTION:The classical method for program analysis by abstract interpret
ation\nconsists in computing a increasing sequence with widening\, which c
onverges towards a correct solution\, then computing a decreasing sequence
of correct solutions without widening. It is generally admitted that\, w
hen the decreasing sequence reaches a fixpoint\, it cannot be improved fur
ther. As a consequence\, all efforts for improving the precision of an ana
lysis have been devoted to improving the limit of the increasing sequence.
In this paper\, we propose a method to improve a fixpoint after its compu
tation. The method consists in projecting the solution onto well-chosen co
mponents and to start again increasing and decreasing sequences from the r
esult of the projection.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:beyene@in.tum.de
CREATED:20140618T074113Z
DTSTAMP:20140618T074113Z
LAST-MODIFIED:20140618T074113Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20140606T143000
DTEND;TZID=Europe/Berlin:20140606T153000
TRANSP:OPAQUE
X-SOGO-SEND-APPOINTMENT-NOTIFICATIONS:NO
END:VEVENT
BEGIN:VEVENT
UID:76F3-572C4D00-1-50A9EF80
SUMMARY:Andreas Lochbihler: Probabilistic functions and cryptographic oracl
es in higher order logic
LOCATION:LMU H1 1311
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160506T075218Z
DTSTAMP:20160506T075218Z
LAST-MODIFIED:20160607T051001Z
DTSTART;TZID=Europe/Berlin:20160603T090000
DTEND;TZID=Europe/Berlin:20160603T100000
TRANSP:OPAQUE
SEQUENCE:1
DESCRIPTION:In this talk\, I am going to present a shallow embedding of a p
robabilistic functional programming language in higher order logic. The l
anguage yields a framework for conducting cryptographic proofs in the comp
utation model and having them checked by a theorem prover. The language f
eatures monadic sequencing\, recursion\, random sampling\, failures and fa
ilure handling\, and black-box access to oracles. Oracles are probabilist
ic functions which maintain hidden state between different invocations. T
o that end\, we propose generative probabilistic systems as the semantic d
omain in which the operators of the language are defined. We prove that t
hese operators are parametric and derive a relational program logic for re
asoning about programs from parametricity.
ATTACH:https://www7.in.tum.de/~schulzef/2016-06-03-Andreas-Lochbihler.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:78B0-56F3E480-1-679BB900
SUMMARY:Rob Lewis: Automation and Computation in the Lean Theorem Prover
LOCATION:TUM MI 00.09.038
DESCRIPTION:Lean is a new proof environment being developed at Microsoft Re
search. Based on dependent type theory\, Lean combines an efficient elabor
ation process with a powerful type class inference mechanism. We describe
how these features have been used in the development of the standard libra
ry\, and why they make Lean a good environment for general automated metho
ds. Ultimately\, Lean aims to bridge the gap between user-centric interact
ive theorem proving and machine-centric automated theorem proving. We also
outline a novel automated procedure for proving inequalities over the rea
l numbers that is currently being implemented.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160324T125948Z
DTSTAMP:20160324T125948Z
LAST-MODIFIED:20160324T125948Z
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
DTSTART;TZID=Europe/Berlin:20160330T143000
DTEND;TZID=Europe/Berlin:20160330T153000
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
UID:798B-53E0E880-1-64D1F680
SUMMARY:Marta Kwiatkowska: Automated Verification and Strategy Synthesis fo
r Probabilistic Systems
LOCATION:TUM MI 02.07.014
CLASS:PUBLIC
CREATED:20140805T142336Z
DTSTAMP:20140805T142336Z
LAST-MODIFIED:20141110T140640Z
DTSTART;TZID=Europe/Berlin:20141107T100000
DTEND;TZID=Europe/Berlin:20141107T110000
TRANSP:OPAQUE
DESCRIPTION:Probabilistic model checking is an automated technique to verif
y whether a probabilistic system\, e.g.\, a distributed network protocol w
hich can exhibit failures\, satisfies a temporal logic property\, for exam
ple\, the minimum probability of the network recovering from a fault in a
given time period is above 0.98. Dually\, we can also synthesise\, from a
model and a property specification\, a strategy for controlling the system
in order to satisfy or optimise the property\, but this aspect has receiv
ed less attention to date. In this paper\, we give an overview of methods
for automated verification and strategy synthesis for probabilistic system
s. Primarily\, we focus on the model of Markov decision processes and use
property specifications based on probabilistic LTL and expected reward obj
ectives. We also describe how to apply multi-objective model checking to i
nvestigate trade-offs between several properties\, and extensions to stoch
astic multi-player games.
SEQUENCE:3
ATTACH:http://www.model.in.tum.de/~schulzef/2014-11-07-Marta-Kwiatkowska.pd
f
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:7C11-56DE8F80-1-73907200
SUMMARY:Eugen Zalinescu: Failure-aware Runtime Verification
LOCATION:MI 02.07.014
DESCRIPTION:Prior runtime-verification approaches for distributed systems a
re limited as they do not account for network failures and they assume tha
t system messages are received in the order they are sent. To overcome thi
s limitation\, we present an online algorithm for verifying observed syste
m behavior at runtime with respect to specifications written in the real-t
ime logic MTL that efficiently handles out-of-order message deliveries and
operates in the presence of failures. It uses a three-valued semantics f
or MTL\, where the third truth value models knowledge gaps\, and it resolv
es knowledge gaps as it propagates Boolean values through the formula stru
cture.\n\n(This is joint work with David Basin and Felix Klaedtke.)
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160308T084700Z
DTSTAMP:20160308T084700Z
LAST-MODIFIED:20160317T131314Z
DTSTART;TZID=Europe/Berlin:20160309T100000
DTEND;TZID=Europe/Berlin:20160309T110000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2016-03-09-Eugen-Zalinescu.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:7DD2-5846D200-AB-1438F4C0
SUMMARY:David Müller: Markov Chains and Unambiguous Büchi Automata
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20161206T145805Z
DTSTAMP:20161206T145805Z
LAST-MODIFIED:20170220T090301Z
DTSTART;TZID=Europe/Berlin:20170224T100000
DTEND;TZID=Europe/Berlin:20170224T110000
TRANSP:OPAQUE
DESCRIPTION:Unambiguous automata are automata with at most one accepting ru
n for every word subsuming deterministic automata. They enjoy being applic
able in case where non-deterministic automata do not fit\, e.g.\, probabil
istic model checking.\n\nIn this talk I will explain a polynomial time-bou
nded algorithm for probabilistic model checking of discrete-time Markov ch
ains against unambiguous Büchi automata specifications and compare it with
known approaches for deterministic omega-automata\, unambiguous automata
over finite words and separated automata.
LOCATION:TUM MI 00.09.038
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
UID:7F12-566EE700-9-2BFC5F00
SUMMARY:Doreen Heusel: Weighted Unranked Tree Automata over Tree Valuation
Monoids
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20151214T155757Z
DTSTAMP:20151214T155757Z
LAST-MODIFIED:20160118T090233Z
DTSTART;TZID=Europe/Berlin:20160115T100000
DTEND;TZID=Europe/Berlin:20160115T110000
TRANSP:OPAQUE
LOCATION:TUM MI 02.07.014
DESCRIPTION:Recently\, the investigation of formal languages of unranked tr
ees has found much attention due to the development of XML and the fact th
at XML-documents can be formalized as unranked trees. With the help of wei
ghted automata on unranked trees over semirings which were introduced by D
roste and Vogler (2011)\, one can investigate quantitative questions on XM
L-documents. In order to obtain a logic counterpart for their weighted unr
anked tree automata\, Droste and Vogler presented a weighted monadic secon
d order (MSO) logic for unranked trees. Their automata capture the express
iveness of their logic but surprisingly not the other way around. We intro
duce a new behavior of weighted unranked tree automata and prove a charact
erization of this behavior by two fragments of weighted MSO logic and ther
eby provide a solution of the open equivalence problem of Droste and Vogle
r. The characterization works for valuation monoids as weight structures\;
they include all semirings and\, in addition\, enable us to cope with ave
rage. Moreover\, we investigate the supports of weighted unranked tree aut
omata and show that the support of a weighted unranked tree automaton over
a zero-sum free\, commutative strong bimonoid is recognizable.
SEQUENCE:1
ATTACH:https://www7.in.tum.de/~schulzef/2016-01-15-Doreen-Heusel.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:A06-572B7480-1-1CB5AD60
SUMMARY:Michael Blondin: Approaching the Coverability Problem Continuously
LOCATION:TUM MI 02.07.014
DESCRIPTION:The coverability problem for Petri nets plays a central role in
the verification of concurrent shared-memory programs. However\, its high
EXPSPACE-complete complexity poses a challenge when encountered in real-w
orld instances. In this talk\, I will present a new approach to this probl
em which is primarily based on deciding coverability in continuous Petri n
ets as a pruning criterion inside a backward framework. A cornerstone of t
his approach is the efficient encoding into SMT of a recently developed po
lynomial-time algorithm for reachability in continuous Petri nets. We will
see that this approach decides significantly more instances than existing
tools on standard benchmarks\, and is in addition often much faster.\n\nJ
oint work with Alain Finkel\, Christoph Haase and Serge Haddad
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20160505T163308Z
DTSTAMP:20160505T163308Z
LAST-MODIFIED:20160513T065744Z
DTSTART;TZID=Europe/Berlin:20160511T160000
DTEND;TZID=Europe/Berlin:20160511T170000
TRANSP:OPAQUE
ATTACH:https://www7.in.tum.de/~schulzef/2016-05-11-Michael-Blondin.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:B85-558BB800-27-4CE8DD00
SUMMARY:Tobias Nipkow: Mining the Archive of Formal Proofs
LOCATION:LMU D Z007
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20150625T081401Z
DTSTAMP:20150625T081401Z
LAST-MODIFIED:20150629T081333Z
DTSTART;TZID=Europe/Berlin:20150703T083000
DTEND;TZID=Europe/Berlin:20150703T093000
TRANSP:OPAQUE
DESCRIPTION:The Archive of Formal Proofs is a vast collection of computer-c
hecked proofs developed using the proof assistant Isabelle. We perform an
in-depth analysis of the archive\, looking at various properties of the pr
oof developments\, including size\, dependencies\, and proof style. This g
ives some insights into the nature of formal proofs.
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:BBA-58B94A00-53-1B74E480
SUMMARY:David de Frutos: Understanding (Concurrent) Process Semantics [firs
t talk]
DESCRIPTION:Once asynchronous parallellsm induces non-determinism\, the sem
antics of concurrent systems becomes difficult to precise. Several framewo
rks to state that semantics have been considered\, and in any one of them
a lot of different semantics have been proposed. In our seminar we will pr
esent a unified approach\, where all these semantics can be presented\, so
that the differences and similarities between them can be captured in an
easy way. Besides\, this unified approach allows generic studies where the
properties of all the semantics can be stated and proved once and for all
\, thus avoiding the disturbing repetitions of the same arguments that we
usually find in the literature\, when any of these semantics is studied in
isolation.
CLASS:PUBLIC
X-SOGO-COMPONENT-CREATED-BY:schulzef@in.tum.de
CREATED:20170303T104906Z
DTSTAMP:20170303T104906Z
LAST-MODIFIED:20170324T161928Z
DTSTART;TZID=Europe/Berlin:20170317T100000
DTEND;TZID=Europe/Berlin:20170317T113000
TRANSP:OPAQUE
SEQUENCE:2
LOCATION:TUM MI 00.09.038
ATTACH:https://www7.in.tum.de/~schulzef/2017-03-17-David-de-Frutos.pdf
BEGIN:VALARM
TRIGGER;VALUE=DURATION:-P1D
ACTION:DISPLAY
END:VALARM
END:VEVENT
X-WR-CALNAME:Talks (ppuma )
END:VCALENDAR