Csanád Telbisz
Csanád Telbisz
This pull request contains an abstraction-aware partial order reduction for the XCFA project. More details about the algorithm can be found in my Scientific Students' Association Report.
Two variables with the same name (but different values) can be put in the explicit state. This may result in a false unsafe verdict (with an incorrect counterexample). A function...
This PR contains a generic ordering consistency checker for concurrent systems with a proof-of-concept implementation for sequential C programs in the xcfa subproject. (Merge #258 first.)
It would be nice to have validation rules for configurations. Basic functionality is currently available on xcfa-refactor branch. Could be further improved with error/warning levels: e.g., INCOMPATIBLE (error), EXPERIMENTAL, NOSUPPORT...
Data race detection should be extended to support pointers (retrieving exact points-to information). This may not be trivial. Or: throw an exception when a pointer is encountered and the property...
The way ArgNodes are compared is practically a depth-first ARG search from the given ArgNodes (cf. [line 284](https://github.com/csanadtelbisz/theta/blob/274e775283feebd93c7b6ef4b9595041a21acb77/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java#L284) comparing outEdges of ArgNodes and [line 33](https://github.com/csanadtelbisz/theta/blob/274e775283feebd93c7b6ef4b9595041a21acb77/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgEdge.java#L33) comparing the targets of ArgEdges)....
**SysML v2 API and Services version:** 2022-05 (on Jun 17, 2022) **Steps to reproduce:** - Using the api client, create a non-empty project (e.g. an empty commit). - Send a...
Recursive structs cannot be parsed correctly, e.g., try this: ```c extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; typedef struct Node { int data; struct Node*...
Currently, traces can be built from a sequence of states and actions. However, this more-or-less assumes an analysis that uses actions (i.e., the LTS), but we have quite some analyses...
Keep UnsupportedInitializer in the init expr so that an exception is thrown when the initializer expression is actually evaluated during an analysis. Passes should remove unsupported initializers - whenever they...