BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1337
DTSTAMP:20230925T045659Z
SUMMARY:Harnessing Multiple BMC Engines Together for Efficient Formal Verif
 ication
DESCRIPTION:Speaker: Ansuman Banerjee (Indian Statistical Institute\, Kolka
 ta)\n\nAbstract: \nIn recent times\, Bounded Model Checking (BMC) engines 
 are gaining wide prominence and showing great effectiveness in formal veri
 fication. Today\, an arsenal of different BMC engines exist\, differing wi
 dely in the optimization\, representations and solving mechanisms used to 
 represent and navigate the underlying state transition system as they look
  for property violations. When having a concrete verification task at hand
 \, a designer is often confronted with the problem of engine selection\, a
 nd more often than not\, has to resort to manually designed selection heur
 istics or machine-learned strategies using carefully selected features of 
 the design. It has often been observed that these different engines have d
 ifferent strengths and weaknesses\, depending on the nature of the verific
 ation task\, the property and the complexity of the design. This talk will
  present a recent work that was set off to examine if combinations of thes
 e engines can help to combine the strengths. We talk about a recent work f
 rom our group that proposes an approach to create a sequencing of BMC engi
 nes that can reach better depths in formal verification\, as opposed to ex
 ecuting them alone. Our approach uses machine learning\, specifically\, th
 e Multi-Armed Bandit paradigm of Reinforcement Learning\, to predict the b
 est-performing BMC engine for a given unrolling depth of the underlying de
 sign transition system. We present an evaluation of our approach to show t
 hat our proposed approach outperforms state-of-the-art BMC engines in term
 s of the depth reached or time taken to deduce a property violation on the
  Hardware Model Checking Competition (HWMCC) benchmarks.\n
URL:https://www.tcs.tifr.res.in/web/events/1337
DTSTART;TZID=Asia/Kolkata:20231017T160000
DTEND;TZID=Asia/Kolkata:20231017T173000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR