Hernan Ponce de Leon
Hernan Ponce de Leon
[This paper](https://www.soundandcomplete.org/papers/POPL2022/NT/NT-POPL2022.pdf) extends TSO with support for non-temporal stores and different kind of memory types (e.g. uncatchable). It would be interesting to add support for this to dartagnan.
I have been taking a look to [this](https://github.com/UniVE-SSV/lisa) library for static analysis which is based on [this](https://iris.unive.it/retrieve/handle/10278/3741476/243041/3460946.3464316.pdf) paper. The library already has implemented several analyses that would be useful for...
According to [this](https://link.springer.com/chapter/10.1007%2F978-3-642-39799-8_9) (page 149, point 1), the fact that a load reads-from exactly one store is guaranteed by the totality of `co` and the definition of `fr`, so we...
The problem is due to the way we handle returns in the boogie code. Currently we assume there is only one return. The file mentioned in the title shoes that...
Under Power, the `TwoSolvers` can easily handle the test `/litmus/PPC/Dart-ctrl-two-regs.litmus`. However both `IncrementalSolver` and `AssumeSolver` get stuck. The problem happens in the `javasmt` branch and it is not reproducible in...
CVC4 results in a segmentation fault for many of the wmm benchmarks. Since the result is neither `FAIL` or `PASS`, the `SVCOMPRunner` keeps increasing the bound and iterates for ever....
Currently the tool can be configure in many ways - passing options - setting flags in `GlobalSettings` - setting flags in `Settings` Now that we use `org.sosy_lab.common.configuration.Configuration` we can move...
We should log some warning to be able to spot potential problems. At least the following ones - mixing theories because of bitwise operations - interpreting `__VERIFIER_assume` and `assume_abort_if_not` as...
Currently we use the "compilation pass" for two different things 1. Go from C level instructions (e.g. atomic_load) to hardware instructions 2. Go from hardware instructions (Xchg) to our IR...
I am trying to understand if the property `sref