Events

Invited Speakers

• Michael Leuschel (Institut für Informatik, Heinrich-Heine-Universität Düsseldorf, Germany)
  
  Solving Set Constraints in B and Event-B: Foundations and Applications
  
  Abstract. This talk will given an overview of how ProB solves set constraints, including sets with mathematical integers, higher-order sets, and sets with complex data types. We also touch on how to deal with large or potentially infinite sets and how to do functional programming in B. We will examine practical applications of set constraint solving, from data validation, to (runtime) model execution over to symbolic model checking and proof support. We will also touch upon other formal methods such as Alloy or TLA+, as well as other constraint solving backends for B, not based on Prolog (SAT via Alloy’s Kodkod API and translations to SMT using Z3 and CVC4).