Search results

Disallow extends for objects and only with case objects

Status: Open.

#1642 In epfl-lara/stainless;

· samuelchassot opened on Mar 18, 2025

Introduce Hylo style aliasing and Hylo input

aliasingAlias and effect analysis for imperativeAlias and effect analysis for imperative

feature

imperative

Status: Open.

#1638 In epfl-lara/stainless;

· vkuncak opened on Jan 27, 2025

Option to block type encoding

doableDoable in short time given right understandingDoable in short time given right understanding

feature

Status: Open.

#1636 In epfl-lara/stainless;

· vkuncak opened on Jan 21, 2025

Comprehensive wrapper for covariant immutable Seq of Scala library

feature

Status: Open.

#1633 In epfl-lara/stainless;

· vkuncak opened on Jan 16, 2025

Add explicit unrolling annotation of loops and recursion

doableDoable in short time given right understandingDoable in short time given right understanding

enhancement

Status: Open.

#1631 In epfl-lara/stainless;

· vkuncak opened on Jan 14, 2025

Contribution Guide

Status: Open.

#1630 In epfl-lara/stainless;

· SidonieBouthors opened on Jan 13, 2025

ghost fields can lead to different runtime behaviour when using equality

bug

ghost

Status: Open.

#1628 In epfl-lara/stainless;

· samuelchassot opened on Jan 7, 2025

Crash when no verification files are provided

Status: Open.

#1625 In epfl-lara/stainless;

· fengwz17 opened on Dec 20, 2024

opaque traits without type encoding

feature

Status: Open.

#1612 In epfl-lara/stainless;

· vkuncak opened on Dec 6, 2024

systematic inline defs handling and interaction with @opaque. Do not repeat while loop transform

feature

Status: Open.

#1611 In epfl-lara/stainless;

· vkuncak opened on Dec 6, 2024

Partial correctness with defined_f predicates

feature

Status: Open.

#1609 In epfl-lara/stainless;

· vkuncak opened on Dec 5, 2024

Support scalaCheck for properties

feature

Status: Open.

#1608 In epfl-lara/stainless;

· vkuncak opened on Dec 5, 2024