|
|
|
| SyncGen | syncgen | Automatic synchronization code generation |
| SpEx | spex | Specification Extensions for Bogor |
| Spec Patterns | patterns | Property specification for finite-state verification. |
| SpAda | spada | SpAda is an Eclipse plug-in for developing applications in SPARK -- a subset of Ada for high assurance applications developed by Praxis High Integrity Systems. SpAda provides integrated support for the Praxis SPARK Examiner -- a static checking tool that enforces very coding rules and information flow requirements. SpAda is integrated with AdaCore's GNATBench Eclipse plug-in for Ada.
Future versions of SpAda will provide advanced analysis capabilities to aid developers in constructing information flow specifications based on SPARK's "derives" annotations.
Our ultimate vision involves extending SpAda so that it becomes an integrated development environment that specifically targets development of information assurance applications in SPARK.
|
| Software Model Checking | smc | Software Model Checking course |
| Site News Admin | newsadmin | |
| Site Admin | siteadmin | The Site Admin project is devoted to the administration of the Santos lab projects site. |
| Sireum | sireum | Sireum software analysis platform |
| SAnToS | santos | The Laboratory for Specification, Analysis, and Transformation of Software (SAnToS Laboratory) conducts both theoretical and applied research on a range of topics in programming language semantics, analysis, and software engineering. |
| PRiMO | primo | <b>Predictable and Reliable Multiagent Organization<\b> |
| Org Model for Adaptive Computational Sys | omacs | Organization Model for Adaptive Computational Systems |
| LYE: High Performance SOAP | lye | LYE is a high-performance SOAP implementation, incorporating multi-level object serialization caching and template-based XML response generation, while maintaining complete protocol compliance. |
| KSUSNS - KSU Sensor Networks | ksusns | The KSUSNS project is the central point of collaboration for all of our sensor network work. This includes contributions from many departments and colleges at KSU including the SAnToS lab, Dan Andresen, Gurdip Singh, and Scott DeLoach. |
| JMLEclipse | jmleclipse | This is an open project for a combined to effort to build an Eclipse plugin for JML that would handle all aspects: parsing, type checking, compilation and run time checking. |
| Indus | indus | A program analysis and transformation toolkit for Java. |
| Human Robot Teams (HuRT) | hurt | HuRT: Human - Robot Teams
HuRT is designed to allow human operators to control teams of cooperative robots at a variety of levels, which includes the organizational level. |
| GudangBogor | gudangbogor | Bogor Extension Repository |
| Goal Model for Dynamic Systems | gmods | Goal Model for Dynamic Systems |
| FRAMES | neo | FRAmework for Model-driven Event diStribution. |
| Courses | courses | The courses project will host all the course material for the various courses taught by the SAnToS Laboratory. This includes courses taught at KSU and UNL. |
| Cooperative Robotics Organization Simula | cros | The Cooperative Robotics Organization Simulator (CROS) allows users to test robot organization algorithms in a controlled environment. This simulator and its accompanying Organization Model was designed and developed at the Kansas State University Multiagent and Cooperative Robotics Laboratory as part of an NSF grant.
The Cooperative Robotics Organization Simulator and Organizational Model provides a sophisticated framework for testing algorithms and applications of multi-agent optimization and structuring. The model defines the agent organization structure, along with the system goals, while the simulator computes the results of the experiments in pseudo real-time. |
| Cadena | cadena | Cadena is an Eclipse-based extensible integrated modeling and development framework for component-based systems. |
| Bogor | bogor | Bogor is a highly customizable and modular model checking framework aimed to ease the development of robust and efficient domain-specific model checkers for verification of dynamic and concurrent software. |
| Bandera Environment Generator | beg | Bandera Environment Generator (BEG) enables modular model checking of Java fragments by generating universal environment models, synthesizing models from user specs, or extracting models from environment implementation. |
| Bandera | bandera | Bandera is a toolset for providing verification and validation for developers of Java applications. |
| ArchiveCrawler | archivecrawler | ArchiveCrawler is a heavyweight web crawler that is based on the Heretrix project by the Internet Archive (makers of the Wayback Machine). |
| Arana | arana | Arana provides a framework and static analysis checks to help ensure quality Java software. |
| agentTool | agenttool | An Eclipse-based integrated design environment to help users analyze, design, and implement multiagent systems. |
| abc Transposer | abctrans | Utility to transpose abc-formatted music files |
| AAAI-Robotics | aaai | This project is the repository for code developed at KSU for the purpose of the AAAI Robot Challenge |
|
To search for projects, please enter the criteria in the text box and press "Search" to get the results
