Search results

UnifLogic: change predicates to assume that path constraints hold

Status: Open.

#67 In katamaran-project/katamaran;

· skeuchel opened on Nov 10, 2025

Working minimal Example

Status: Open.

#62 In katamaran-project/katamaran;

· capt-hb opened on Jun 10, 2025

·  

Binary BlockVerifier

Split (possible) Non-Terminating functions from terminating ones

Status: Open.

#61 In katamaran-project/katamaran;

· capt-hb opened on Jun 10, 2025

·  

Binary BlockVerifier

Better binoptel_eq_dec implementation for update_vector_subrange

Status: Open.

#52 In katamaran-project/katamaran;

· capt-hb opened on Mar 6, 2025

Reintroduce parametrization over exec_call in shallow soundness proof

Status: Open.

#51 In katamaran-project/katamaran;

· skeuchel opened on Feb 28, 2025

Speed up bitvector enumeration with difference lists

Status: Open.

#50 In katamaran-project/katamaran;

· skeuchel opened on Feb 25, 2025

Define NamedEnv directly instead of deriving it from Env

Status: Open.

#47 In katamaran-project/katamaran;

· skeuchel opened on Dec 7, 2023

Split positions of all user-defined predicates into input and outputs

Status: Open.

#45 In katamaran-project/katamaran;

· skeuchel opened on Nov 14, 2023

Pattern matching on enums with a list of alternatives

Status: Open.

#44 In katamaran-project/katamaran;

· skeuchel opened on Nov 9, 2023

Avoid decidable equality for type indices in symbolic formula equality function

Status: Open.

#42 In katamaran-project/katamaran;

· skeuchel opened on Nov 7, 2023

Avoid decidable equality for type indices in binary op case of symbolic term equality function

Status: Open.

#41 In katamaran-project/katamaran;

· skeuchel opened on Nov 7, 2023

Introduce intermediate symbolic proposition interface in the symbolic executor

Status: Open.

#40 In katamaran-project/katamaran;

· skeuchel opened on Oct 18, 2023