is a high-assurance system engineering platform incorporating various formal analyses
and compilation toolchains. Read more...
Presentations: Slang@ISoLA21, HAMR@ISoLA21, Logika@TCCoE22
HAMR is a high-assurance model-based rapid engineering toolset for embedded systems (next-gen).
Logika is a program verifier and proof checker for propositional,
predicate, and programming logics (v3).
Awas is an information flow analyzer and visualizer for component-based systems (v3).
Amandroid (now Argus-SAF)
is a static analysis framework for security vetting Android apps (v2).
Department of Computer Science
Kansas State University