mc-imperial/jfs

Issues

• jfs-smt2cxx can't handle all formulas that jfs can

  #39 opened 4 years ago by moyix
  3

• EqualityExtractionPass should propagate equalities

  #38 opened 5 years ago by delcypher
  0

• Is it possible to extend JFS to process string constraints?

  #37 opened 5 years ago by lingjunz
  1

• Submit to SMT-COMP 2020

  #36 opened 5 years ago by jryans
  0

• Update to the latest Z3 release

  #35 opened 5 years ago by jryans
  0

• Update to latest LLVM/Clang/LibFuzzer release

  #34 opened 5 years ago by jryans
  0

• Experiment with optimization levels

  #33 opened 5 years ago by jryans
  0

• Experiment with inline coverage counters

  #32 opened 5 years ago by jryans
  0

• Experiment with comparison tracing

  #31 opened 5 years ago by jryans
  0

• Experiment with LibFuzzer's value profile

  #30 opened 5 years ago by jryans
  0

• Implement optimal BufferElement packing algorithm for BufferAssignment

  #29 opened 5 years ago by jryans
  0

• Implement a special case in runtime Buffer reading functions for byte aligned access

  #28 opened 5 years ago by jryans
  0

• Implement custom LibFuzzer mutators

  #27 opened 5 years ago by jryans
  0

• Implement parallel fuzzing

  #26 opened 5 years ago by jryans
  0

• Implement porfolio solver backend

  #25 opened 5 years ago by jryans
  0

• Extend EqualityExtraction to support equalities with conversions

  #24 opened 5 years ago by jryans
  0

• Support lowering `fp.eq` to `=` in cases that EqualityExtraction can fire

  #23 opened 5 years ago by jryans
  0

• Implement public C API and library

  #22 opened 5 years ago by jryans
  0

• Hooks up to KLEE

  #21 opened 5 years ago by jryans
  0

• Estimate constraint difficulty using #SAT

  #20 opened 5 years ago by jryans
  0

• Experiment with comparison branch splitting LLVM pass

  #19 opened 5 years ago by jryans
  0

• Experiment with comparison branch splitting LLVM pass

  #18 opened 5 years ago by jryans
  0

• JFS's handling of fp.min and fp.max is unsound.

  #17 opened 5 years ago by jryans
  0

• Platform behaviour divergence when generating seeds

  #16 opened 5 years ago by jryans
  0

• Supporting quantified formulas?

  #13 opened 6 years ago by rainoftime
  1

• Minor error in README

  #15 opened 6 years ago by shaobo-he
  0

• jfs-opt removes relevant commands

  #14 opened 6 years ago by shaobo-he
  1

• ScopedTimerImpl deadlocks when pinned to single CPU

  #10 opened 7 years ago by delcypher
  1

• Custom mutators

  #9 opened 7 years ago by delcypher
  0

• Constraint independence

  #7 opened 7 years ago by delcypher
  0

• Equality hints via compiler transformations and value profiling

  #8 opened 7 years ago by delcypher
  0

• Experiment with optimization levels

  #6 opened 7 years ago by delcypher
  0

• Implement support for "maximum number of constraints solved"

  #5 opened 7 years ago by delcypher
  0

• Implement support for custom seeds

  #4 opened 7 years ago by delcypher
  0

• Implement model extraction and validation

  #3 opened 7 years ago by delcypher
  0

• Implement the Serebryany encoding

  #2 opened 7 years ago by delcypher
  1

• Gather additional solvers and configurations for experiments

  #1 opened 7 years ago by delcypher
  0