Selected Projects
- Circuzz: A fuzzer for processing pipelines of zero-knowledge circuits (artifact)
- LaZ: An extension of Nomos for lazy testing of machine-learning models
- Sherlock: An interrogation-testing framework for testing program analyzers (artifact)
- Minotaur: A constraint-based program generator for testing program analyzers (artifact)
- Olympia: A benchmarking platform for Solidity fuzzers
- GreenBench: A green fuzzer-benchmarking platform
- Nomos: A specification language and framework for expressing and testing k-safety properties of machine-learning models
- DLSmith: A dependency-aware metamorphic-testing framework for Datalog engines
- π-fuzz: A metamorphic-testing framework for action policies
- SmartACE: A compositional verifier for smart contracts (artifact)
- queryFuzz: A metamorphic-testing framework for Datalog engines
- Neuro-aware program analyzer: A static analyzer for verifying system properties of programs invoking neural networks
- tAIlor: A framework for automatically tailoring an abstract interpreter to the code under analysis and any given resource constraints (artifact)
- LIBRA: A static-analysis framework for certifying fairness of deep neural networks (artifact)
- STORM: A blackbox mutational fuzzer for SMT solvers
- DeepSearch: A blackbox attack for deep neural networks
- bran: A static-analysis framework for EVM bytecode
- α-Diff: A framework for differentially testing soundness and precision of program analyzers