Prove almost-arbitrary multi-relational invariant sets overlap

GoogleCodeExporter commented 9 years ago

A few meetings ago we have determined that the sets of multi-relational 
invariants may overlap almost-arbitrarily. That is, an invariant like "a AFby 
b" that is in the set of {t} relation invariants may or may not appear in the 
set of {r,t} invariants, depending on what the input traces.

Tim needs to complete a formal proof of this almost-arbitrary overlap with 
examples for the overlaps, and a proof by contradiction for the one 
non-overlapping region that we've found.

Original issue reported on code.google.com by bestchai on 26 Apr 2012 at 7:09

GoogleCodeExporter commented 9 years ago

Original comment by bestchai on 27 Apr 2012 at 2:32

Attachments:

multir_invariant_sets_whiteboard.jpg

GoogleCodeExporter commented 9 years ago

Please review
https://bitbucket.org/bestchai/synoptic-tim-honors-thesis/changeset/1b163fba0380

Original comment by T.101.JV on 30 Apr 2012 at 4:16

ModelInference / synoptic

Prove almost-arbitrary multi-relational invariant sets overlap #250