Software
Tools for runtime verification, model checking, and reasoning about software.
Projects · newest first
TaskSAT
Model, schedule, and verify task networks with temporal and resource constraints.
Fuzzing
Generate tests using constraints, including temporal constraints on event sequences.
LogScope / C++
The C++ LogScope project and its repositories.
PyContract
Write monitors in Python to check event traces and detect violations of expected behavior.
MonAmI
Monitoring for First-Order Allen Temporal Logic. I contributed the parser and mentored the work.
F Prime Scala
A Scala implementation of the F Prime flight software framework.
DejaVu
Check first-order temporal properties over event streams, using binary decision diagrams to represent observed data.
nfer
Turn detailed event traces into higher-level intervals that describe patterns of activity.
K
The K language project.
Daut
Combine state machines, temporal operators, and rules to monitor streams of events.
LogFire
A rule-based approach to monitoring event streams, built around a variation of the RETE algorithm.
TraceContract
Specify trace properties with data-parameterized automata and temporal logic in a Scala DSL.
LogScope / Python
A monitoring framework for checking execution logs against specifications.
Java PathFinder 1 (JPF1)
The original Java-to-Promela model checker, with its user guide and papers.
Garbage collector refinement
A mechanized refinement proof for a garbage collection algorithm.