Software & Tools
- CARTS (Compositional Analysis of Real-Time Systems)
- Architecture aware analysis of concurrent software (Checkfence)
- We partner with Fremont Associates to provide tool support for analysis of embedded systems architectures expressed in the AADL modeling language. Formal schedulability analysis algorithms are implemented in the Furness toolset.
- An industrial case study is starting in collaboration with Honeywell, which aims at the modeling and analysis of wireless architectures.
- Automated symbolic compositional verification by learning assumptions, JIST (Interfaces for Java classes using abstraction and games)
- Specification, Analysis, and Testing of Scenario-based Requirements
- HERMES (Model Checking of Hierarchical State Machines)
- Mocha (Model checking of open systems using ATL)
- CHARON (Hybrid systems: modeling and verification)
- Timed and hybrid automata
