The Formal Methods Alliance brings researchers from many theoretical and formal disciplines together. Our goal is to advance the state of the art in computer systems by using methods of theoretical computer science, software engineering, and computational science and engineering. The members of the group bring a refreshing divergence of views to the problems of hardware and software development.
Paul advocates the use of formal methods, based on mathematical models, for developing correct (or reliable) systems. As part of this work, he promotes the use of object oriented techniques (which help us to structure our software models) and unified semantics (which help the many different users of the models - man and machine - to communicate). This work also incorporates analysis of different computational models and complexity of algorithms. Paul is also interested in the triangular relationship between research, teaching and technology transfer. Currently he is investigating the best ways of teaching formal methods: to students and to software engineers. When interfacing with the real world, he tends to work in the domain of telecommunications.
I am currently supervising 3 Irish PhD students and 3 French masters students.
Personal Pages
Contact Paul Gibson
Steve's research interests include the design and analysis of algorithms and computation theory. In particular, he is interested in developing mathematicial models for difficult combinatorial and computational optimization problems. He also has interests in parallel algorithms, approximation algorithms, genetic algorithms, and, in computation theory: abstract models of computation and questions of ambiguity. He recently co-authored two texts in the area of domination in graphs, the first is: Fundamentals of Domination in Graphs, Marcel Dekker, 1998, co-authored with Teresa Haynes and Peter Slater.
Personal Pages
Contact Steve Hedetniemi
Jeff's research is in reverse mathematics, a program of mathematical logic founded by H. Friedman and S. Simpson. Basically, he measures the exact logical strength of familiar theorems by formalizing them and proving equivalence results within a hierarchy of axiom systems for second order arithmetic. Sometimes this kind of analysis can indicate computable restrictions for noncomputable theorems.
Personal Pages
Contact Jeff Hirst
My area of interest is design of algorithms. Most of my algorithmic work has been algebraic, graph theoretic, or combinatorial. In the last two years I have written a series of papers with R. Jamison on the so-called equal union property for hypergraphs. Given a hypergraph (i.e. a family of sets), the problem asks to decide if there exist two disjoint sets of edges having equal unions. There is a nice connection between this problem and so-called sign-nonsingular matrices. Although the general problem is NP-complete, we have discovered several situations which guarantee a polynomial time algorithm. I have one Phd student (Ted Doyle) at the moment. His research has to do with graph partitioning. He is trying to identify certain classes of graphs that generalize biparitite graphs, yet can be recognized in polynomial time.
Many complexity problems have their origin in the types of problems studied by this group.
Personal Pages
Contact Dave Jacobs
My research extends to several areas of computer science, including language and compiler techniques, software engineering and simulation modeling. I have developed techniques for compiler optimization including instruction scheduling, parallelization and cache optimization. I have developed program representations to facilitate analysis and optimization; these representations include program dependence graphs for imperative and object-oriented software. A current project is to construct a class hierarchy graph for object-oriented programs and map the structure of the program to the intermediate and assembly code representation; this mapping enables program optimizations that exploit the structure of the source code.
Personal Pages
Contact Brian Malloy
PhD (Computer Science) Dublin City University
Rosemary's current research interests include formal methods of program derivation and specification, program transformation, theorem proving and program construction. She is particularly interested in the formalisation of object oriented specifications as much of today's software is written in object oriented languages such as C++ or Java. She has recently commenced a PhD on this topic in the School of Computer Applications, Dublin City University.
As a result of this research, she aims to develop an object-oriented specification language that provides a mathematical basis for object-oriented programs, thus ensuring that object-oriented software is designed in a precise unambiguous manner. She is also interested in developing a program construction theory, which will be used to formally develop object-oriented programs from these specifications.
Personal Pages
Contact Rosemary Monahan
My focus is formal methods using the pi-calculus and linear logic, mainly applied to communications protocols. Some of this work is done in conjunction with the IMPROVE project, a research collaboration between NUI Maynooth and DCU. I am also interested in parsers and compiler technology for object-oriented languages, particularly Java and C++ Formal Specification using constructive logic and the Coq proof environment. At various times I've also worked with formal semantics, compilers and fuzzy logic.
Personal Pages
Contact James Power
Sitaraman currently supports a research associate/ Ph. D. student and expects to hire another GRA beginning Spring 2001. In the last 3 years, he hoas supported 3 post-doctoral research associates and graduated 3 Ph. D. students.
Component-based software engineering (CBSE) is the focus of the Reusable Software Research Group (RSRG) at Clemson. Together with the RSRG at Ohio State University, we have defined RESOLVE to facilitate CBSE. RESOLVE includes a framework to support specification and implementation of components, a prescriptive discipline for component design, and a notation for describing components with properties including maximum generalization, efficiency, and modular verification.
The Software Composition Workbench (SCW) is a programming environment for constructing verifiable component based software in RESOLVE. The workbench comprises a number of tools: a reasoning tool, integrated with the PVS theorem prover, to perform composition and correctness proofs; a compilation tool to support Ada, C++ and Java back ends; and a composition tool to instantiate and compose generic components from a library of over 100 formally-specified reusable components.
Personal Pages
Contact Murali Sitaraman
Steve's research is motivated by the verification, validation, and accreditation of scientific simulations. An escapee from the original Bell Labs in 1980, Steve has a PhD degree in mathematics specializing in numerical analysis. He also participates in foundations of mathematics activities. All this leads to an interest in probability and the general study of uncertain systems. His formal study is the use of Carnap-Hempel logic and Dempster-Shafer concepts of uncertainty to the validation of uncertain systems from the observers' point of view.
Steve is also involved nationally in the National Science Foundation's Corporation and Foundation Alliance as a member of the board of the Shodor Education Foundation. The Alliance strives to revitalize the nation's undergraduate education enterprise, to increase the quality and quantity of graduates entering the workforce who are well prepared in science, mathematics, engineering and technology (SMET).
He currently has three MS students.
Contact Steve Stevenson
Personal Pages