Email:
kfoury at bu dot edu

URL: http://www.cs.bu.edu/~kfoury/

Office: (617) 353-8911; MCS Room 201 C

Fax: (617) 353-6457

Office hours: Tuesday, Thursday, 2:30-4:30 pm

TEACHING

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:

RESEARCH

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:

- 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.

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
2020.01.14* .