Ali Kheradmand

Issue with LTL Automizer

2

The following code breaks with nullPointerException in LTL Automizer's [online interface](https://monteverdi.informatik.uni-freiburg.de/tomcat/Website/?ui=int&tool=ltl_automizer). ``` //@ ltl invariant inv: [](AP(load_below_threshold == 1)); int load_below_threshold = 1; void check_property(int* router_load){ int p = 1;...

Strange behavior of proof mode

3

I am using k-legacy the latest commit. I have the following definition and spec: ``` module TEST syntax Val ::= "@undef" syntax Val ::= NUVal syntax NUVal ::= "@val" "("Int","Int","Bool")"...

I am trying to use KEQ for establishing equivalence between two programs written in two languages: ``` module COMMON syntax Vals ::= @nil ... endmodule module L1 imports COMMON ......

Problem in ConstrainedTerm.evaluateConstraints

1

I can not give a small example here, but sometimes when I use krun, a rule that I expect to apply, does not get normally applied, but when I use...

I have a [configuration](https://github.com/kframework/p4-semantics/) like following: ``` @resetArrays ( SetItem ( extra ) ) ~> ... ... extra |-> $array ( 4 , 0 , -1 ) ``` And I...

I have a [configuration](https://github.com/kframework/p4-semantics) that contains the following cells: ``` ... .K .K .Map .Map .K ``` Note ` .Map ` And I have the following rule ``` rule @processDec(counter...

"List [ Int ]" (sometimes) yields ListItem

2

Hi I have the following configuration ``` @val ( 0 , 14 , false ) ~> @deref ( sel_profile , 0 ) ~> @setCrntRule ( . ) ~> @setCrntTable (...

Rule gets applied once, but not again

4

I have a configuration like this: ``` ... 0 @nextPacket ... packet ... 1 @nextPacket ... . ... ... ``` And I have a rule like this ``` rule @nextPacket...

I have a simple configuration like this: ``` configuration $PGM:P4Program ``` When I run it with a P4 program (i.e the one [here](https://github.com/kframework/p4-semantics/blob/master/test/semantics/basic_routing/basics_routing.p4)), it works without any problems. But If...

Problem with symbolic execution

11

For my P4 semantics, I use string of 0s and 1s as input and the rules convert parts of this string to integer using String2Base. Concrete interpretation works fine but...