ftsrg/theta

Issues

• A* search strategy integration

  #214 opened a year ago by leventeBajczi
  3

• Collect and add recent Theta papers to list of publications (Help wanted: add yours!)

  #328 opened 16 days ago by AdamZsofi
  1

• Remove superfluous modulo operators from XCFA

  #327 opened 16 days ago by AdamZsofi
  0

• Use runexec in the portfolio (XCFA portfolio improvement)

  #326 opened 16 days ago by AdamZsofi
  0

• Witnesses get wrong programfile names when using portfolio (xcfa-cli)

  #295 opened 3 months ago by AdamZsofi
  0

• xcfa-cli issue: UNSAT_CORE refinement tries to use ItpRefToPtrPrec and crashes

  #300 opened 2 months ago by AdamZsofi
  0

• XSTS-cli: Verifying a model with syntax errors should fail

  #303 opened 2 months ago by arminzavada
  0

• IMC vs. RIMC finds loops at different times

  #319 opened 16 days ago by leventeBajczi
  1

• General/instance vars in precision

  #247 opened a year ago by s0mark
  0

• Configuration rules

  #249 opened 16 days ago by csanadtelbisz
  0

• Improve local variables by introducing a new Decl for them

  #263 opened 8 months ago by mondokm
  1

• Initializers cannot use other global vars in c frontend

  #266 opened 8 months ago by leventeBajczi
  0

• Some solvers failing XstsTest

  #268 opened 5 months ago by RipplB
  11

• JavaSMT term transforming: inproper handling of function declarations

  #270 opened 5 months ago by RipplB
  3

• Pointers + data race

  #236 opened 16 days ago by csanadtelbisz
  0

• Support new witness format

  #221 opened 16 days ago by leventeBajczi
  1

• Create final portfolio

  #220 opened 16 days ago by leventeBajczi
  0

• Enhance logging, add diverse exit codes

  #217 opened 16 days ago by leventeBajczi
  0

• BMC, k-induction

  #215 opened 16 days ago by leventeBajczi
  0

• Support sensible safety witnesses

  #211 opened 16 days ago by leventeBajczi
  0

• Use a more generic checkstyle-based formatting solution

  #195 opened 16 days ago by leventeBajczi
  0

• ArgNode comparison is practically a DFS search of the ARG

  #203 opened 16 days ago by csanadtelbisz
  0

• The WebDebuggerLogger is always enabled and it is responsible for a considerable portion of runtime.

  #208 opened 16 days ago by leventeBajczi
  0

• Fix concurrency witnesses

  #242 opened 16 days ago by AdamZsofi
  0

• Log level affects Z3 behavior

  #246 opened a year ago by s0mark
  0

• Floating point type sometimes reports a significand of size N + 1 instead of N

  #257 opened 8 months ago by leventeBajczi
  0

• PRED_SPLIT produces false negative results for XCFA

  #267 opened 6 months ago by leventeBajczi
  2

• Solver executables - permission and packaging issues

  #298 opened 3 months ago by AdamZsofi
  0

• `theta-analysis` depends on concrete solver implementations

  #273 opened 5 months ago by mondokm
  0

• Update SV-COMP configuration files to use the new flags

  #297 opened 16 days ago by AdamZsofi
  0

• Suggestion to improve implementation of IMC

  #299 opened 3 months ago by blishko
  1

• XSTS: support choice-else operations

  #302 opened 2 months ago by arminzavada
  3

• XSTS-cli: Allow the specification of the verification property in the XSTS file

  #301 opened 2 months ago by arminzavada
  1

• Allow "$" in XSTS variable names

  #265 opened 4 months ago by mondokm
  0

• Sequence interpolation with SMTInterpol

  #253 opened 8 months ago by RipplB
  0

• Urgent init location in XTA

  #245 opened a year ago by szdan97
  0

• Progress Check

  #219 opened a year ago by leventeBajczi
  6

• Struct flattening and initialization support

  #210 opened a year ago by leventeBajczi
  3

• Update .xml, .yml, .py, ....

  #218 opened a year ago by leventeBajczi
  0

• Remove unusable logging from C frontend (warning-hell)

  #225 opened a year ago by leventeBajczi
  0

• SMT solver refresh (if necessary)

  #213 opened a year ago by leventeBajczi
  5

• Iron out bugs on last year's tasks

  #222 opened a year ago by leventeBajczi
  1

• Test full configs on last year's tasks

  #212 opened a year ago by leventeBajczi
  2

• Find out how to do pre-runs (somehow via coveriteam)

  #216 opened a year ago by leventeBajczi
  3

• Concurrency Witness Validation

  #223 opened a year ago by leventeBajczi
  1

• Wrong result is given for the unreach-call property

  #209 opened a year ago by leventeBajczi
  3

• New benchmarks from CHC-COMP

  #224 opened a year ago by leventeBajczi
  0

• Some pthread functions are not supported (cond_signal) by the frontend

  #206 opened a year ago by leventeBajczi
  0

• Projection should be given in XcfaAnalysis.getXcfaAbstractor in order to avoid performance degradation

  #207 opened a year ago by leventeBajczi
  2

• New benchmarks (CHC)

  #205 opened a year ago by leventeBajczi
  0