runtimeverification/k

Issues

• [K-Bug] Broken condition for heating rules with result

  #4683 opened a month ago by virgil-serbanuta
  0

• [K-Bug] Cannot generate bison parser or glr-bison parser

  #4678 opened 2 months ago by Stevengre
  1

• [K-Bug] The LLVM backend ignores rule priorities

  #4676 opened 2 months ago by virgil-serbanuta
  0

• `kdist` isn't as flexible as makefile

  #4669 opened 2 months ago by Stevengre
  2

• Improve the performance of `kompile`

  #4668 opened 2 months ago by Stevengre
  2

• A difficult-to-reproduce segmentation fault.

  #4672 opened 2 months ago by Stevengre
  0

• Improved interpreter error messages for quicker error identification

  #4670 opened 2 months ago by Stevengre
  0

• [K-Bug] <pyk coverage runerror>

  #4664 opened 2 months ago by nn020701
  0

• Wrong type annotations in pyk

  #4660 opened 2 months ago by pxhdev
  0

• Understanding the `bmc-depth` bottleneck

  #4658 opened 3 months ago by PetarMax
  0

• Support for syntactic simplifications

  #4579 opened 5 months ago by PetarMax
  21

• CTerm.match_with_constraint does not return expected CSubst.constraints

  #4496 opened 3 months ago by Stevengre
  4

• Tips for using K

  #4655 opened 3 months ago by Stevengre
  0

• Add `pyk` support for terms with parametric sorts

  #4653 opened 3 months ago by tothtamas28
  0

• Cell extraction and substitution in Kore.

  #4652 opened 3 months ago by Stevengre
  0

• How to automatically generate the python bindings from the semantics?

  #4649 opened 3 months ago by Stevengre
  0

• What is `KCFG.Cover.csubst` supposed to be?

  #4602 opened 3 months ago by Stevengre
  3

• Optimize `cterms_anti_unify`

  #4642 opened 3 months ago by Stevengre
  2

• Polish list lookup patterns

  #4640 opened 3 months ago by dwightguth
  0

• [K-Bug] ClassCastException for #as and cells

  #4638 opened 4 months ago by virgil-serbanuta
  0

• Add test for T-division op.s using LLVM `interpreter`

  #4629 opened 4 months ago by jberthold
  0

• Potential bug in how integer division/modulus are encoded to SMT

  #4606 opened 4 months ago by ehildenb
  2

• Remove final uses of `run_process`

  #4627 opened 4 months ago by ehildenb
  0

• [K-Bug] Python code should use version number from pyproject.toml

  #4614 opened 4 months ago by 0cjs
  0

• [K-Bug] AssertionError for incomplete rule

  #4613 opened 4 months ago by virgil-serbanuta
  0

• [K-Bug] Broken MInt literal parsing

  #4609 opened 4 months ago by virgil-serbanuta
  0

• Automatically verifying the correctness of simplification rules.

  #4604 opened 4 months ago by Stevengre
  2

• [K-Bug] Uncaught exception thrown of type NegativeArraySizeException

  #4592 opened 4 months ago by pxhdev
  8

• [Question] How to Replace the outdated [structural] Attribute in K Framework?

  #4594 opened 4 months ago by liuliuliu401
  1

• Check that tokens are non-empty after `#Layout`

  #4595 opened 4 months ago by Scott-Guest
  0

• Make use of parsing caches in kdist

  #4481 opened 4 months ago by dwightguth
  2

• Support the `"assume-defined"` parameter of `"implies"`

  #4570 opened 4 months ago by geo2a
  1

• A shallow embedding of K definitions into Lean 4

  #4552 opened 5 months ago by tothtamas28
  1

• [K-Bug] Broken "Non-exhausive match" warning

  #4587 opened 4 months ago by virgil-serbanuta
  0

• [K-Bug] kgdb.py fails to print after single steps

  #4576 opened 5 months ago by pxhdev
  3

• [K-Improvement] Metadata attribute

  #4568 opened 5 months ago by sskeirik
  0

• PyPi Pyk repo has accidental release in it

  #4553 opened 5 months ago by Baltoli
  2

• Better experience when `kdist` reports compiler error from `kompile`

  #4564 opened 5 months ago by dwightguth
  0

• K Webpage: Add links to github source pages for the tutorials and user manual.

  #4549 opened 5 months ago by nishantjr
  0

• Guide: Debugging an issue across the RV stack

  #4542 opened 5 months ago by Baltoli
  4

• Non-determenism in the defintion of `minInt`

  #4543 opened 5 months ago by geo2a
  0

• Collisions between LLVM bindings and static symbols in host programs

  #4523 opened 5 months ago by Baltoli
  0

• [K-Bug] The debugger reports "No source file named definition.kore."

  #4540 opened 5 months ago by pxhdev
  1

• [K-Bug] Kompile crash instead of error for [left] attribute

  #4536 opened 5 months ago by virgil-serbanuta
  0

• [K-Bug] Example of a symbol used in `overload` attributes not appearing.

  #4515 opened 5 months ago by gtrepta
  2

• Disallow sorts with case-insensitive equal names

  #4508 opened 6 months ago by Baltoli
  4

• `llvm_interpret` logs are very verbose

  #4516 opened 5 months ago by gtrepta
  0

• `pyk prove` cannot handle claims with `#Equals` in `requires`

  #4495 opened 6 months ago by nwatson22
  3

• CTerm.anti_unify doesn't provide expected constraints for CTerm and CSubst.

  #4502 opened 6 months ago by Stevengre
  2

• Simplify option parsing code in pyk

  #4484 opened 6 months ago by dwightguth
  1