Papers for

software model checkers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Undecidable to find polyhedral invariants in linear programs

The existence of polyhedral invariants is undecidable for linear systems

Abstract: The existence of polyhedral inductive invariants suitable for proving that a given control location is unreachable is undecidable for programs using only linear arithmetic over Z or Q, by reduction from 2-counter machines.

Fri 25 SeptLogic in Computer Science

The gist

Sometimes computer programs need special rules, called invariants, to prove certain parts of the program can never be reached. This paper shows that when programs use only simple math with whole or fractional numbers, it is impossible to always decide if such rules exist. The researchers used a known hard problem involving simple machines with two counters to prove this. This means there are limits to what automatic tools can verify about some programs.

Open → 2609.31146v1