Porous Invariants
| Autor: | Engel Lefaucheux, Joël Ouaknine, David Purser, James Worrell |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering 020207 software engineering 0102 computer and information sciences 02 engineering and technology 01 natural sciences Computer Science::Databases Logic in Computer Science (cs.LO) |
| Zdroj: | Computer Aided Verification Lecture Notes in Computer Science Computer Aided Verification ISBN: 9783030816872 Lecture Notes in Computer Science-Computer Aided Verification Computer Aided Verification-33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part II |
| ISSN: | 0302-9743 1611-3349 |
| Popis: | We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; these invariants are not necessarily convex, and can in fact contain infinitely many 'holes'. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle (non-)reachability questions for various interesting classes of affine loops and target sets. Full version of paper to appear at CAV 2021 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|