BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Model Checking: SMT-Based Software Model Checking - Dirk Beyer (Lu
 dwig-Maximilians-Universität München)
DTSTART:20220722T150000Z
DTEND:20220722T154500Z
UID:TALK176747@talks.cam.ac.uk
DESCRIPTION:There are several successful SMT-based model-checking approach
 es for software verification\,&nbsp\;including bounded model checking (BMC
 )\, predicate abstraction\, IMPACT\, k-induction\,&nbsp\;property-driven r
 eachability (IC3)\, and interpolation-based model checking (IMC).&nbsp\;We
  have implemented all six algorithms in the open-source verification frame
 work CPAchecker\,&nbsp\;and give an overview over their performance charac
 teristics.&nbsp\;
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR