PhD in Computing

42003 - Logic and Algebra in Computer Science (LAI)


  • Type: Elective
  • Semester: S3
  • ECTS: 6
  • Teaching Points: 15
  • Offer: Annual
  • Responsible Unit: CS
  • Responsible: Albert Oliveras
  • Language: English
  • Requirements: Students are expected to have the same level they would reach with the subject of Logic of this master. They should also have some basic knowledge of data structures, algorithms and algorithms complexity.

GOALS
The aim of this course is to provide deeper insights into the role of logic in computer science, and to give an overview of new foundations and methods as well as of industrial logic-based and algebra-based applications. In particular, this course will provide the student with the necessary experience for choosing logic-based tools for handling a given problem, at the right levels of expressive power of the logic and the complexity of the associated deductive or decision problems.

CONTENTS
1. Short reminder on propositional and first-order logic
  • Syntax and semantics
  • Resolution
2. SAT-based techniques
  • DPLL systems with conflict analysis
  • OBDDs
  • Extensions of DPLL and BDDs: AllSAT, Max-SAT
  • Applications to verification
3. SAT modulo theories (SMT)
  • SMT with arrays, lists, integers and reals
  • Reductions to SAT. Eager methods
  • Lazy Methods. DPLL(T)
  • Applications to CSPs and combinatorial optimization problems
4. Other extensions SAT and SMT
  • Pseudo-Boolean-based techniques (0-1 integer programming)
  • QBF and the polynomial hierarchy
  • Applications to logic synthesis
5. Applications to verification tools
  • Predicate Abstraction
  • Tools for the automatic verification of industrial code (Intel, Microsoft), such as SLAM or Blast

DOCENT METHODOLOGY
The 6 ECTS of this subject are divided in different types of activities: lectures on theory and problems (TP), laboratory lessons (LAB), studying and solving problems with notes, articles and book chapters and exercise lists (EST), an implementation project (IMP) and an evaluation test (AVAL).

TP lectures will introduce fundamental concepts and the solutions of proposed problems will be revised.

At LAB lessons, practical problem resolution exercises will be proposed, using tools such as SAT/SMT/QBF solvers or logical programming with restrictions.

EVALUATION METHODOLOGY
Evaluation will take into account the different activities done along the course.

At the end of the course, there will be a written exam that basically consists of solving problems similar to those done in the course.

Implementation projects must be handed out in class to the teacher. Students will have to explain them and answer the teacher’s questions.

BIBLIOGRAPHY

RESOURCES
Rooms with terminal for laboratories (1 hour per week or 2 hours bimonthly). Materials prepared by the teacher will be available for students (copies of manuscript notes or of transparencies used in class, and exercise lists).

WEBSITE