Projects
Current Projects
This project provides open-source Medical Device Coordination Framework (MDCF) for exploring solutions related to designing, implementing, verifying, and certifying, systems of integrated medical devices.
http://mdcf.santos.cis.ksu.edu/
JMLEclipse is, first and foremost, an Eclipse-based JML front-end that provides JML infrastructure to process JML specifications at source (JML2 syntax) and bytecode (embedded JML Intermediate Representation -- JIR) levels.
http://jmleclipse.projects.cis.ksu.edu/
Sireum is a long-term research effort to develop an over-arching software analysis platform that incorporates various static analysis techniques such as data-flow framework, model checking, symbolic execution, abstract interpretation, and deductive reasoning techniques.
http://www.sireum.org/
Past Projects
The goal of the Bandera project is to integrate existing programming language processing techniques with newly developed techniques to provide automated support for the extraction of safe, compact, finite-state models that are suitable for verification from Java source code.
http://bandera.projects.cis.ksu.edu/
Bogor is an Eclipse-ready extensible and customizable model checking engine for object-oriented (OO) software.
http://bogor.projects.cis.ksu.edu/
Cadena is a sophisticated Eclipse-based IDE for specification, analysis, and development of distributed systems built using the CORBA Component Model (CCM).
http://cadena.projects.cis.ksu.edu/
Indus is a collection of static analysis and program transformation libraries for full Java that includes Kaveri -- an Eclipse-based user interface that provides a number of capabilities for computing program slices and navigating and querying program dependence graphs.
http://indus.projects.cis.ksu.edu/
Spec Patterns an online repository for information about property specification for finite-state verification. The intent of this repository is to collect patterns that occur commonly in the specification of concurrent and reactive systems.
http://patterns.projects.cis.ksu.edu/
The project aims to use object-oriented methodologies to design high-assurance systems using: (1) high-level, modular specification of global, cross-cutting synchronization aspects, (2) automatic derivation and weaving of verifiable synchronization code, and (3) automated verification of critical safety/liveness properties of woven code.
http://syncgen.projects.cis.ksu.edu/
