Miscellaneous Projects
Here are some of the other areas I've worked in:
The size of ordered binary decision diagrams (BDDs) is sensitive to the variable ordering that is
chosen. Finding an optimal variable ordering is NP-complete.
I investigated two approaches to tackling the BDD variable ordering problem: (1) Finding approximation
algorithms, and (2) Using machine learning. Unfortunately, neither approach was very successful.
Approximation hardness: The following report gives some approximation hardness results for problems
in Boolean function complexity.
The
Hardness of Approximating Minima in OBDDs, FBDDs and Boolean functions.
S. A. Seshia and R. E. Bryant.
Computer Science Department technical report CMU-CS-00-156, August 2000.
Machine learning for BDD variable reordering: The main idea was to use a decision tree-based algorithm
to learn position and grouping information that could be used in sifting. Minor improvements in
the stability of the sifting algorithm were obtained. This work, done in 1999, remains unpublished.
Robust implementation of geometric algorithms requires the use of exact arithmetic.
Since exact arithmetic is expensive, one must use it only when
finite-precision arithmetic proves to be inadequate.
Two techniques for uncovering this inadequacy are
interval arithmetic and error analysis.
We did a performance study of these two alternatives with respect to the line-side
and in-circle geometric predicates, and reported the results in the following technical report.
A
Performance Comparison of Interval Arithmetic and Error Analysis in Geometric
Predicates.
S. A. Seshia, G. E. Blelloch,
and R. W. Harper.
Computer Science Department Technical report CMU-CS-00-172, December 2000.
In a term paper, I explored a hierarchical technique for verifying microelectromechanical system (MEMS) designs
via simulation.
The basic idea was to translate a full-scale schematic into a reduced-order model, and then simulate this model
rather than the original, detailed schematic. The simulation results of the reduced-order model were comparable
to those of the original schematic while being faster by a factor of about 100.
Hierarchical Verification for Microelectromechanical Systems.
S. A. Seshia.
Unpublished manuscript, December 1998.
My B.Tech. (senior undergraduate) thesis was in the area of multisensor data fusion.
The thesis reviewed literature on sensor input synchronization, image registration (alignment) and image fusion.
A new algorithm for image registration was proposed and implemented, and formal evaluation criteria for
image fusion algorithms were given.
Multisensor Image Alignment and Fusion.
S. A. Seshia.
B. Tech. thesis, April 1998.
We compared two approaches to formal verification of cryptographic protocols: theory generation
and model checking. Based on this comparison, we proposed a combination of the two methods.
A Comparison and Combination of Theory Generation and Model Checking
for Security Protocol Analysis.
Nicholas J. Hopper, Sanjit
A. Seshia, Jeannette M. Wing.
In Workshop on Formal Methods in Computer Security (FMCS), July 2000, Chicago.
Associated with Intl. Conf. on Computer-Aided Verification (CAV'00).
An earlier version appeared as a CMU CS technical report.
Combining
Theory Generation and Model Checking for Security Protocol Analysis.
Nicholas J. Hopper, Sanjit A. Seshia, Jeannette M. Wing.
Computer Science Department technical report CMU-CS-00-107, January
2000.
Esterel is a synchronous, textual language for programming reactive systems. Statecharts is a graphical
language for specifying reactive systems. The paper below gives a translation of Statecharts to
Esterel so as to avail of both the visual power of Statecharts and the verification tools available with
Esterel.
A Translation of Statecharts to Esterel.
S. A. Seshia, R. K. Shyamasundar,
A. K. Bhattacharjee and S. D. Dhodapkar.
In Proceedings of the World Congress on Formal Methods, FM'99, Toulouse,
France, LNCS vol. 1709, Sept. 1999, pp.983-1007.
My co-authors implemented and deployed a tool called PERTS based on the above translation. Here is a
paper that describes this tool.
PERTS: A Graphical Environment for the Specification and Verification of Reactive
Systems.
A. K. Bhattcharjee, S. D. Dhodapkar, S. A. Seshia and R. K. Shyamasundar.
Journal of Reliability Engineering and System Safety, 71 (3), 2001,
pp. 299 -310 , Elsevier Science.(corrigendum in vol. 72)
An earlier conference version is available here:
A Graphical Environment for the Specification and Verification of Reactive
Systems.
A.K. Bhattcharjee, S.D. Dhodapkar, S.A. Seshia and R.K. Shyamasundar.
In Proceedings of SAFECOMP'99, Toulouse, France. LNCS vol. 1698, Sept.
1999, pp. 431-444.