BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Uniform Reduction to SAT and SMT 
DTSTART:20110620T161500
DTSTAMP:20260510T165031Z
UID:c8a5ea52341d5a21468a36d66d67c584a2862ab7f4a568690a194cf6
CATEGORIES:Conferences - Seminars
DESCRIPTION:Prof. Predrag Janicic\, University of Belgrade\nSAT is a probl
 em of satisfiability in propositional logic\, and the satisfiability modul
 o theory (SMT) is a problem of satisfiability with respect to a background
  theory (e.g.\, linear arithmetic\, theory of arrays) expressed in classic
 al first-order logic with equality. Over the last decade\, SAT and SMT sol
 vers made tremendous advances both in theoretical and in practical aspects
 . They have a wide range of applications\, primarily in software verificat
 ion\, planning\, scheduling\, cryptanalysis\, electronic design automation
 \, etc. Typically\, problems are reduced to SAT/SMT by problem-specific\, 
 ad-hoc tools. In this talk\, a general framework\, URSA Major\, for reduci
 ng problems to SAT/SMT will be presented. The system can be also considere
 d as a general modelling system for specifying and solving a wide class of
  problems (e.g.\, NP problems). The specification language is C-like\, but
  based on a novel imperative-declarative programming paradigm. A problem i
 s specified by a test (expressed in an imperative form) that given values 
 indeed make a solution to the problem. From a problem specification\, a co
 rresponding propositional or first-order formula (in a suitable theory) is
  generated and passed to a SAT/SMT solver. If the formula is satisfiable\,
  then its model is transformed back to the values of the unknowns. The sys
 tem will be illustrated by examples from several domains.  Prof. Janicic's
  homepage
LOCATION:BC 01 https://plan.epfl.ch/?room==BC%2001
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR