Showing cs.LOShow all
3 papers · 1 filter
cs.LO2025★ 1 cited
U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
Flavio Ascari, Roberto Bruni, Roberta Gori +1
O'Hearn's Incorrectness Logic (IL) has sparked renewed interest in static analyses that aim to detect program errors rather than prove their absence, thereby avoiding false alarms…
cs.LO2023
Sufficient Incorrectness Logic: SIL and Separation SIL
Flavio Ascari, Roberto Bruni, Roberta Gori +1
Sound over-approximation methods have been proved effective for guaranteeing the absence of errors, but inevitably they produce false alarms that can hamper the programmers. Conver…
cs.LO2023
Exploiting Adjoints in Property Directed Reachability Analysis
Mayuko Kori, Flavio Ascari, Filippo Bonchi +3
We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley's property directed reachability algorithm. For finding safe invariants or counterexamples, the f…