Software
Tools for runtime verification, model checking, and reasoning about software.
Projects · newest first
DejaVuMT
Monitor event traces with first-order temporal logic, extending DejaVu with future and timed operators. Uses Z3 or CVC5 to reason about data and infer constraints on symbolic time bounds.
TaskSAT
Model, schedule, and verify task networks with temporal and resource constraints.
TaskTree
Organize tasks in an unlimited hierarchy and filter by today, this week, importance, and more. Edit tasks directly in filtered views while keeping the original hierarchy in sync.
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
K is a textual language for modeling systems and writing formal specifications, combining ideas from programming and modeling languages. Its tools support type checking and use the Z3 SMT solver to check consistency and correctness of models.
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.