User Tools

Site Tools


deltacheckissues

DeltaCheck Summarizer Issue Tracking

Status: OPEN, WORK, DONE, CLOSED, SUSPENDED

Priority: HIGH (<1 week), MEDIUM (<3 weeks), LOW (>3 weeks)

Priority Issue Affected code base Raised by Assigned to Status
MEDIUM better information reuse in binary search Martin Peter DONE
HIGH control MiniSat branching heuristics for diverse models solvers Martin Saurabh WORK
HIGH full strategy iteration binary search domains Peter Peter WORK
MEDIUM invariant reuse in unwindings domains Saurabh Saurabh WORK
HIGH predicate abstraction solver and domain domains Peter Cristina WORK
HIGH custom templates Peter Peter WORK
HIGH next_var in custom templates Peter Peter WORK
HIGH disjoint finitely disjunctive domains domains Peter Peter WORK
HIGH refinement for non-monotonic conditions domains Peter OPEN
HIGH general template solver domains Peter OPEN
HIGH substitution-based concretisation in domains domains Peter OPEN
MEDIUM inferring disjunctive preconditions domains Peter OPEN
MEDIUM refactoring for product domains domains Peter OPEN
MEDIUM testing precondition inference regression Peter Lihao OPEN
MEDIUM debug equalities domains Peter OPEN
MEDIUM enum support in templates template_generator, util Peter OPEN
MEDIUM assign nondet to all uninitialized local variables (needed for unwinder) Saurabh OPEN
MEDIUM pointer parameters local_ssa Peter OPEN
MEDIUM float tests regression Peter OPEN
MEDIUM Debian benchmarking Peter OPEN
MEDIUM Merge context sensitivity into summary branch Peter OPEN
LOW Yices backend Peter Martin OPEN
LOW use MiniSAT simplifier Peter OPEN
LOW list length instrumentation goto-instrument Peter OPEN
LOW incremental context sensitivity summarizer Peter OPEN
LOW smash array instrumentation goto-instrument Peter Peter SUSPENDED
LOW improve templates involving index expressions (see array_safe5) Peter OPEN
LOW recursion summarizer Peter OPEN
LOW struct members in arrays ssa_analyzer Peter OPEN
LOW mixed type templates (floats) template_domain Peter OPEN
LOW C type promotion vs type extensions in template computations template_domain Peter OPEN
LOW variable packing heuristics ssa_analyzer Peter OPEN
LOW user-defined templates ssa_analyzer Peter OPEN
LOW template generation heuristics ssa_analyzer Peter OPEN
LOW summary DB JSON export/import Peter OPEN
rename nondet_symbols ssa_unwinder Peter Saurabh CLOSED
domain for NULL pointer information equality_domain Peter Peter CLOSED
global variables in SSA ssa Peter Daniel CLOSED
fix nested loop unwinding ssa_unwinder Peter Peter CLOSED
Incremental assertion checks summary_checker Peter Peter CLOSED
turn SSA nodes map into list local_ssa Daniel Peter CLOSED
move renaming map into domain domains Peter Peter CLOSED
tool integration for ranking function synthesis Peter Peter CLOSED
Refactoring for incremental unwinding ssa_unwinder Peter Saurabh CLOSED
k-induction loop summary_checker Peter Peter CLOSED
ranking function domain linrank_domain Peter Hongyi CLOSED
ranking function solver ranking_solver Peter Cristina CLOSED
deltacheckissues.txt · Last modified: 2014/12/11 11:16 by schram