Thomas Haas
Thomas Haas
I have an abstraction refinement procedure which iteratively queries the SMT-solver, and in the case of SAT, explores the model returned by the solver to generate refinement clauses. From the...
The [configuration option file](https://sosy-lab.github.io/java-smt/ConfigurationOptions.txt) lists ways to pass additional options to the various underlying solvers, however, it does not list `Z3`. Is it possible to pass arbitrary options to `Z3`?...
Right now, Dartagnan overapproximates the set of all possible addresses but to do so, it uses two assumptions: - There is a fixed and known number of mallocs - Each...
This PR adds a pass that simplifies the following types of code ``` lbl1; // Any jump to lbl1 can get forwarded to jump directly to lbl2 lbl2; ``` and...
Code that contains multiple labels with the same name causes various problems: - The parsing generates bogus code if the same label name is used in _different_ threads. This should...
I took a look into the special events we generate for C-Litmus (Linux) tests as they do not compile to our internal LISA-like core language. These special events consist of...
On the Linux github repo, there is a very detailed section about its memory model [LKMM](https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/tools/memory-model). Importantly, - it contains the official `.cat` file for linux kernel memory model. -...
The encoding we use for thread creations involves creating write-read-pairs. While our encoding does not strictly enforce a spawned thread to actually run (i.e. read the write that activates it),...
Right now, we construct the whole memory representation during parsing. Problem: We lose all information of when memory gets allocated. A particular use case is Escape Analysis which could be...
This is an extension of #39. Context: We currently have 2 types of expressions BExpr and IExpr. IExpr can either represent a mathematical integer or a bit vector expression. However,...