Science Department, Boston
kfoury at bu dot edu
Office: (617) 353-8911; MCS Room 201 C
Fax: (617) 353-6457
Office hours: Tuesday, Thursday, 2:30-4:30 pm
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.
In the Spring 2019 semester, I co-taught with
Kinan Dak Albab:
In the Spring 2020 semester, I will teach a junior-level course:
Brief self-introduction, primarily addressed to potential graduate-student
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
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.
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.
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
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,
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,
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,
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,
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.
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