Event Date
Thomas Reps
University of Wisconsin-Madison
What could symbolic model checking, path profiling, and quantum simulation
possibly have in common?
CFLOBDDs are a data structure that is essentially plug-compatible with
Binary Decision Diagrams (BDDs), and hence useful for representing
certain classes of functions, relations, matrices, graphs, etc. in a
highly compressed fashion. CFLOBDDs share many of the good properties
of BDDs, but -- in the best case -- the CFLOBDD for a function can be
exponentially smaller than any BDD for that function. Compared with
the size of the decision tree for a function, a CFLOBDD -- again, in
the best case -- can give a double-exponential reduction in size.
CFLOBDDs have the potential to permit applications to (i) execute much
faster, and (ii) handle much larger problem instances than has been
possible heretofore. However, CFLOBDDs have certain additional
overheads compared with BDDs, so they are only better than BDDs for
representing very large relations. The successful application area we
found is quantum simulation, where the matrices that need to be
represented are huge.
Where does path profiling fit into the story? Come to this talk to
find out!
Joint work with Meghana Aparna Sistla (UT-Austin) and Swarat Chaudhuri
(UT-Austin).
======================================================================
Biographical Sketch:
Thomas W. Reps is the J. Barkley Rosser Professor & Rajiv and Ritu
Batra Chair in the Computer Sciences Department of the University of
Wisconsin, which he joined in 1985. Reps is the author or co-author
of four books and more than two hundred thirty papers describing
his research. His work has concerned a wide variety of topics,
including program slicing, dataflow analysis, pointer analysis, model
checking, computer security, code instrumentation, language-based
program-development environments, the use of program profiling in
software testing, software renovation, incremental algorithms, and
attribute grammars.
Professor Reps received his Ph.D. in Computer Science from Cornell
University in 1982. His Ph.D. dissertation won the 1983 ACM Doctoral
Dissertation Award.
Reps has also been the recipient of an NSF Presidential Young
Investigator Award (1986), a Packard Fellowship (1988), a Humboldt
Research Award (2000), and a Guggenheim Fellowship (2000). He is also
an ACM Fellow (2005). In 2013, Reps was elected a foreign member of
Academia Europaea. Reps received the ACM SIGPLAN Programming Languages
Achievement Award for 2017. With A. Lal, M. Musuvathi, S. Qadeer, and
J. Rehof, Reps received the 2023 CAV Award for the ``introduction of
context-bounded analysis and its application to systematic testing of
concurrent programs.''
Reps has held visiting positions at the Institut National de Recherche
en Informatique et en Automatique (INRIA) in Rocquencourt, France
(1982-83), the University of Copenhagen, Denmark (1993-94), the
Consiglio Nazionale delle Ricerche in Pisa, Italy (2000-2001), and the
University Paris Diderot-Paris 7 (2007-2008). From 1988 to 2019, he
was President of GrammaTech, Inc.