Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Predicate weakening in AbsInt #80

Open
greitsch opened this issue Nov 24, 2016 · 1 comment
Open

Predicate weakening in AbsInt #80

greitsch opened this issue Nov 24, 2016 · 1 comment
Assignees
@Heizmann @danieldietsch @greitsch
Labels
abstract interpretation Automizer enhancement

Comments

@greitsch
Copy link
Member

greitsch commented Nov 24, 2016 •
edited
Loading

Compute the unsat core of all terms part of an obtained counterexample in order to reduce conjuncts in terms.
greitsch added a commit that referenced this issue Mar 22, 2017
@greitsch
Towards AbsInt Unsat Core Computation (#80)
83e6c6d 
The list of interpolants is now more concrete (from IPredicate to
AbsIntPredicate) in order to allow for more functionality and to allow
for computing unsat cores with abstract interpretation.
danieldietsch added a commit that referenced this issue Mar 23, 2017
@danieldietsch
see #80 -- add base class for interpolant weakening
b490b9a
greitsch added a commit that referenced this issue Mar 28, 2017
@greitsch
Added nested classes to handle iterating over counter examples (#80)
b162253
greitsch added a commit that referenced this issue Apr 3, 2017
@greitsch
Updated Interpolant Sequence Weakener (#80)
222c252
danieldietsch added a commit that referenced this issue Apr 3, 2017
@danieldietsch
see #80 -- integrate DummyInterpolantSequenceWeakener into CegarAbsIn…
da2f01b 
…tRunner
greitsch added a commit that referenced this issue Apr 3, 2017
@greitsch
More logic in the HoareTripleChecker for the CEGAR AbsInt Runner (#80)
dacb864
greitsch added a commit that referenced this issue Apr 4, 2017
@greitsch
Added inductivity check for debugging (#80)
2afb560
greitsch added a commit that referenced this issue Apr 6, 2017
@greitsch
Towards interpolant sequence weakening for Taipan (#80)
06021fd
greitsch added a commit that referenced this issue Apr 6, 2017
@greitsch
Interpolant Sequence Weakener now tries to compute the hierarchical p…
007863a 
…restates (#80)
greitsch added a commit that referenced this issue Apr 6, 2017
@greitsch
Towards interpolant sequence weakening (#80).
7bad80d
greitsch added a commit that referenced this issue Apr 7, 2017
@greitsch
Fixed a bug occurring when a state with no variables would be weakened (
71ef7d0 
#80)
greitsch added a commit that referenced this issue Apr 10, 2017
@greitsch
Fixed a bug in the interpolant sequence weakener (#80)
a622f4e
greitsch added a commit that referenced this issue Apr 10, 2017
@greitsch
Fixed a problem with PreStates in the interpolant sequence weakener (#80
49d1309 
)
greitsch added a commit that referenced this issue Apr 11, 2017
@greitsch
Improved interpolant sequence weakening with abstract post (#80)
4a36a0e
@danieldietsch
Copy link
Member

For clarification: this issue is about predicate weakening.

@danieldietsch danieldietsch changed the title Unsat Core Computation for Term-Reduction Predicate weakening in AbsInt Dec 14, 2017
@Heizmann Heizmann self-assigned this Dec 14, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Heizmann Heizmann

@danieldietsch danieldietsch

@greitsch greitsch

Labels
abstract interpretation Automizer enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@Heizmann @danieldietsch @greitsch