Repository navigation

Static property pre-check: SAFE for programs proven free of RuntimeExceptions or AssertionErrors - #73

Closed

nils-loose wants to merge 7 commits into

svcomp27/integrationfrom

feat/property-aware-downgrade

Closed

Static property pre-check: SAFE for programs proven free of RuntimeExceptions or AssertionErrors#73
nils-loose wants to merge 7 commits into
svcomp27/integrationfrom
feat/property-aware-downgrade

Commits on Oct 18, 2026
- Add a static check for uncaught RuntimeExceptions and AssertionErrors
  
  nils-loose
  and
  claude
  committed
  508db53
- Answer SAFE when the property pre-check proves the property
  
  nils-loose
  and
  claude
  committed
  2273466
- Test the property pre-check and the verdict it gives
  
  nils-loose
  and
  claude
  committed
  c41571f
- Check only the static initializers that may run
  
  nils-loose
  and
  claude
  committed
  3445d64
- Close soundness gaps in the exception-freedom check
  
  nils-loose
  and
  claude
  committed
  d0d7357
- Treat calls that a library default method may serve as unknown
  
  nils-loose
  and
  claude
  committed
  1675424
- Fail the check when the JVM would not load the classpath as modelled
  
  nils-loose
  and
  claude
  committed
  9cd00a6