Assaf Kfoury

Professor, Computer Science Department, Boston University

Email: kfoury at bu dot edu
Office: (617) 353-8911; MCS Room 201 C
Fax: (617) 353-6457


Brief self-introduction to my graduate-level teaching, mostly first-year but not only.

In the last 5 years or so, I have put much effort in developing two graduate-level courses on Formal Methods in CS at Boston University. In the BU Catalog, these are CS 511 (offered in fall semesters) and CS 512 (offered in spring semesters). The primary, but not sole, focus of CS 511 is on the theory and practice of SAT/SMT solvers broadly speaking. The primary, but not sole, focus of CS 512 is on various temporal logics and modal logics, and the automated systems based on them. I have referenced a variety of textbooks and papers in these two courses, not necessarily narrowly limited to formal methods (because students need sometimes to be reminded things they learned before in algorithm analysis, or discrete mathematics, or abstract algebra), and I have often written my own lecture notes to present my perspective on some of the material I have taught. I do the latter especially when I think that some of the concepts and their interdependence are not sufficiently stressed in conventional presentations, even though the material may be otherwise standard. For more details on these two courses, and to download lecture notes I have written for them, visit their homepages:

In the two decades preceding my current focus on formal methods, I taught graduate-level courses on other subjects, at BU and other universities (when on sabbatical leave), including on: algorithm design and analysis, foundations of programming languages, and the lambda-calculus (in computer science departments), recursion and computability theory, mathematical logic, and model theory (in mathematics departments). I taught most of the latter in seminar style, for smaller groups of students.


Brief self-introduction, primarily addressed to potential graduate-student supervisees.

My constant research interests since my days in graduate school have been about the many interactions between Mathematical Logic and Computer Science broadly speaking (hereafter: Math Logic in CS), which have thus included such things as type theory, the lambda-calculus, static analysis, recursion theory, and less fashionable areas (yes, there are fashions in scientific research) such as the theory of program schemas (closely related to something called abstract computability and something else called abstract interpretation). From time to time, however, some colleagues or graduate students have pushed me outside the boundaries of Math Logic in CS, into such areas as graph theory and applied algorithms, or mathematical aspects of system networking, and sometimes into areas requiring some system development (coding of software packages), which I appreciate and even enjoy without being very good at it (just as you can enjoy soccer or basketball without being good at it).

So, any time you want to engage me on something related to Math Logic in CS in a broad sense, I would be delighted to respond in kind. If you are interested in knowing what I have been working on in the last five years (outside my teaching duties and my being a faculty member at Boston University), you can take a look at the following reports:

For research I have done before the last five years and going as far back as the 1970's, search me on the Web -- also look up references under my name in the reports listed above.

If you want to know about my style of work, most of my papers and reports are single-authored. If I am part of a multi-authored report, I am rarely the first author. The vast majority of my single-authored reports are at least 20 pages in length. On the spectrum from terse mathematical writing (which can be very clever) to transparent exposition, I strive to be close to the latter and ask for the same from students I supervise (I believe good science is meant to be communicated as transparently as possible, not as tersely and cleverly as possible). All my graduate-student supervisees have produced publishable results, and published them in mainstream venues (such as ACM or IEEE publications) before completing their studies and without my being a co-author in most cases; this is also my preference and, I believe, the way it should be.

This webpage was created on 2018.08.01 and last modified on 2018.09.18 .