counter scalability¶


suite id	`counter_scalability`
domain	manufacturing
language	ST
difficulty	medium
validation status	candidate
origin	authored
license	CC-BY-4.0

Authored by Pierre Dantas for the ESBMC-PLC-Sec curation, adopted into this suite

What is proved¶

From benchmarks/manufacturing/counter_scalability/props.yaml. What each kind claims, and what it becomes on either route, is on The properties we prove.

id	kind	claim	requirement
`P1`	`invariant`	`!(pump && level_high)`	Overflow guard; here evaluated across counter-fuse widths to measure detection cost vs. scale.

Variants¶

file	expected verdict	violates	method
`bomb_N00255.st`	VIOLATION	`P1`	expert
`bomb_N01023.st`	VIOLATION	`P1`	expert
`bomb_N04095.st`	VIOLATION	`P1`	expert
`bomb_N16383.st`	VIOLATION	`P1`	expert
`bomb_N32767.st`	VIOLATION	`P1`	expert

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.9 KB	`64ab0d40a12b`
`bomb_N00255.st`	structured text	1.6 KB	`3c4d3251fd19`
`bomb_N01023.st`	structured text	1.6 KB	`0c4639c80bf4`
`bomb_N04095.st`	structured text	1.6 KB	`19d11a2381b8`
`bomb_N16383.st`	structured text	1.6 KB	`b6e4b9627bc2`
`bomb_N32767.st`	structured text	1.6 KB	`789b97fdae0b`
`props.yaml`	property file	0.2 KB	`453545bb2d6d`

Recorded runs¶

A task can carry two routes. ld is ESBMC's ladder front end reading the program directly. via C is the same solver reached through Beremiz and MatIEC, which is the only route that reaches ST, IL, FBD and SFC; see How ESBMC-PLC works.

counter_scalability__bomb_N00255__viac via C (props.yaml, expected VIOLATION): master SAFE
counter_scalability__bomb_N01023__viac via C (props.yaml, expected VIOLATION): master SAFE
counter_scalability__bomb_N04095__viac via C (props.yaml, expected VIOLATION): master SAFE
counter_scalability__bomb_N16383__viac via C (props.yaml, expected VIOLATION): master SAFE
counter_scalability__bomb_N32767__viac via C (props.yaml, expected VIOLATION): master SAFE