BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
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
SUMMARY:
Approximate counting in SMT and value estimation for probabi
listic programs
STATUS:CONFIRMED
ATTENDEE;CN="Dmitry Chistikov
":
MAILTO:no@spam.com
DESCRIPTION:
#SMT\, or model counting for logical theories\, is a well-kn
own hard problem that generalizes such tasks as counting the
number of satisfying assignments to a Boolean formula and c
omputing the volume of a polytope. In the realm of satisfiab
ility modulo theories (SMT) there is a growing need for mode
l counting solvers\, coming from several application domains
(quantitative information flow\, static analysis of probabi
listic programs). In this work\, we show a reduction from an
approximate version of #SMT to SMT. We focus on the theorie
s of integer arithmetic and linear real arithmetic. We propo
se model counting algorithms that provide approximate soluti
ons with formal bounds on the approximation error. They run
in polynomial time and make a polynomial number of queries t
o the SMT solver for the underlying theory\, exploiting ``fo
r free'' sophisticated heuristics implemented within modern
SMT solvers. We have implemented the algorithms and used the
m to solve a value estimation problem for a model of loop-fr
ee probabilistic programs with nondeterminism. Joint work wi
th Rayna Dimitrova and Rupak Majumdar.
DTSTART;TZID=Europe/Paris:20150602T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201506021
100
UID:LSVsemLSV.201506021100@lsv.ens-cachan.fr
LOCATION:Salle de ConfĂ©rence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR