Miscellaneous Projects

Here are some of the other areas I've worked in:

Binary Decision Diagrams

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.

Computational Geometry

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.


MEMS Design and Verification

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.


Multisensor Data Fusion

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.


Security Protocol Verification

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.


Statecharts and Esterel

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.