Assaf Kfoury
Professor, Computer
Science Department, Boston
University
Email:
kfoury at bu dot edu
URL: http://www.cs.bu.edu/~kfoury/
Office: (617) 353-8911; CDS Room 1010
Fax: (617) 353-6457
WARNING TO STUDENTS: Don't fall prey to
scammers and fraudsters! They are actively targeting students
using fake email addresses. If you receive an unexpected message
claiming to be from me, it is a scam.
I will NEVER send unsolicited emails to students I
do not personally know and will NEVER use an email address
other than mine @bu.edu -- even when not available
during system maintenance.
Table of Contents
TEACHING
(table of contents)
Brief self-introduction to my graduate-level teaching, mostly
first-year but not only.
In the last 5-7 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 and automated proof assistants 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.
In the Spring 2019 semester, I co-taught with
Kinan Dak Albab:
In the Fall 2021 semester, I co-taught a new course with Alley Stoughton.
The course was co-developed with Marco Gaboardi and Alley Staughton:
Between TEACHING and RESEARCH
(table of contents)
From time to time I have produced documents that give a different
perspective and a different organization of known material without
establishing new results. Typical of such documents are graduate-level
tutorials, presentations in research seminars, and reports that go
beyond lecture notes.
-
What Are Proof Assistants? How Do We Use Them? Why Do They Work?,
documents (three .pdf files and three .lean scripts) used
by Assaf Kfoury and Marco Gaboardi for three lectures on
interactive proof assistants, March 16, 19, and 20, 2026.
-
First-Order Term-Rewriting Systems,
a compressed tutorial in coordination with follow-up presentations
by the brilliant mathematician Mirai Ikebuchi:
-
Influences of Computer Science on Modern Mathematical Practices, tutorial
over Zoom in May 2022 to Palestinian students in several colleges
in the West Bank, partly in English and partly in Arabic.
-
Dependently Typed Automated Systems, documents (15 sets of slides, 23 handouts, all
.pdf files) for a one-semester graduate-level course, first given
in Spring 2019.
-
Formal Proof Systems for First-Order Logic,
notes for a graduate-level seminar, written in short and distant spurts
since the 1970's.
RESEARCH
(table of contents)
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:
- String Rewriting Systems: Brief Introduction and Sample of Open Problems -- sample of updated open problems (as of June 2026) related to String Rewriting Systems, August 19, 2026.
- Will Artificial Intelligence Put Mathematicians Out of Work? -- slides and lecture notes I have used in three separate webinars in July and August of 2026, August 28, 2026.
-
أنظمة للبرهنة الاحتمالية -- محاولة لتقديم نظرة عامة لغير المتخصصين Probabilistic Proof Systems -- an attempt at a presentation for the non-experts [original English before translated to Arabic] September 1, 2026. I was not involved in the original research reported in this article, written in English by Oded Goldreich, a top expert in all areas related to probabilistic proof systems. However, producing the Arabic translation still required new research -- not mathematical, but linguistic -- as I had to choose adequate Arabic terms for well-established concepts that had not been named in Arabic before.
- Tertium Non Datur: Driving Force For New, More, & Better Mathematics -- slides of invited talk at Logic in Philosophy, June 6, 2025.
-
Mathematical Logic in Computer Science
(CoRR, /abs/1802.03292, February 2018) --
my perspective on what has been my intellectual home since graduate school.
- Personal Reflections on the Role of Mathematical Logic in Computer Science,
in Fundamenta Informaticae, Vol. 170, no. 1-3, pp 207-221,
October 2019. This is a much shorter and summarized version of the
preceding report, extended to include responses to criticisms of the preceding.
-
Efficient Reassembling of Graphs, Part 1: The Linear Case,
joint with Saber Mirzaei
(CoRR, abs/1509.06434, Sept 2015, shorter version published
in J. of Combinatorial Optimization, 33(3):1057-1089, April 2017) --
optimal reassembling of graphs in general is NP-hard.
- Efficient
Reassembling of Three-Regular Planar Graphs, joint with
Benjamin Sisson (CoRR, abs/1807.03479, July 2018) -- optimal
reassembling of particular classes of graphs can be carried out
efficiently in linear time. Accepted for publication in
J. of Combinatorial Optimization, DOI: 10.1007/s10878-020-00555-7.
Further details are in the project website
Graph Reassembling.
-
A Fixed-Parameter Linear-Time Algorithm for Maximum Flow in Planar
Flow Networks (CoRR, /abs/1807.04186, July 2018) --
submitted to J. of Discrete Algorithms.
-
A Fixed-Parameter Linear-Time Algorithm to Compute Principal Typings
of Planar Flow Networks (CoRR, /abs/1807.07067, July 2018) --
inspired by joint work with Azer Bestavros at the intersection
of formal methods and system networking.
-
Software Inspection System, joint with Mark Reynolds and
Azer Bestavros, published as US Patent 9,495,542 (including
full description of the system), November 2016.
-
A Verification Platform for SDN-Enabled Applications, joint with
Rick Skowyra, Andrei Lapets, and Azer Bestavros, in
Proc. of IC2E 2014: IEEE International Conference on Cloud Engineering,
March 2014.
-
The Syntax and Semantics of a Domain-Specific Language for
Flow-Network Design, in
Science of Computer Programming, Volume 93, pp 19-38, November 2014.
-
Reusable Requirements in Automated Verification of Distributed Systems,
joint with
Rick Skowyra, Andrei Lapets, and Azer Bestavros,
Technical Report BUCS-TR-2013-002, CS Dept., Boston University, February 2013.
-
Verifiably-Safe Software-Defined Networks for CPS, joint with
Rick Skowyra, Andrei Lapets, and Azer Bestavros,
in Proc. HiCoNS 2013: The 2nd ACM International Conference on High
Confidence Networked Systems, April 2013.
-
Postlude: Seamless Composition and Integration -- a Perspective on
Formal Methods Research, joint with
Andrei Lapets and Azer Bestavros,
in Mathematical Structures in Computer Science, 23(04):934-943,
August 2013.
-
Towards Accessible Integration and Deployment of Formal Tools and Techniques,
joint with Andrei Lapets, Rick Skowyra,
and Azer Bestavros, in
Proc. of TOPI 2013: The 3rd Workshop on Developing Tools as Plug-ins,
May 2013.
-
Lightweight and Practical Formal Methods in the Design and Analysis of
Safety-Critical Systems, Special issue of Mathematical Structures in
Computer Science, guest editors: Azer Bestavros
and Assaf Kfoury, Volume 23 - Issue 4, August 2013.
For research I have done before the last 10-15 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 have
an idea of the research I did for my doctoral thesis, which I completed in 1973:
Going further back to 1969, when I had started my graduate studies,
the following is my first publicly available report, issued as a technical report,
that allowed me to say I am interested in computer science
(only because the title includes the expression sequential machine
otherwise the article is really about matrix algebra), itself partly based on a term
project I did for a course taught by Prof. Michael Artin:
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 -- not to deny the possibility of happy occasions
when we are offered mathematical constructions that are both transparent and clever).
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.
After TEACHING and RESEARCH
(table of contents)
My role in the history of the Computer Science Department at Boston University:
-
Tribute to Steve Homer's Career: the Early Years,
text of my oral address on May 22, 2026.
-
Two-day celebration of my role in the history of the CS Department at BU and
in my research areas in general, on June 3-4, 2026:
partial
Collection of
other addresses given by other participants (colleagues, friends, former students), and
Over the years I have been increasingly involved
in philosophical and historial discussions related to the
mathematical sciences. The following are examples:
Non-academic ACTIVISM
(table of contents)
The following are groups and organizations I support and whose reports
I regularly read. I am also member of, and an occasional contributing writer to,
some of them:
This webpage was created on 2018.08.01 and last modified on
2026.09.05 .