9 citations · 36 across the 34 of their papers we have counts for
Showing 2014Show all
3 papers · 1 filter
cs.LO2014
Abstraction Refinement for Trace Inclusion of Infinite State Systems
Radu Iosif, Adam Rogalewicz, Tomas Vojnar
A \emph{data automaton} is a finite automaton equipped with variables (counters or registers) ranging over infinite data domains. A trace of a data automaton is an alternating sequ…
cs.FL2014
Interprocedural Reachability for Flat Integer Programs
Pierre Ganty, Radu Iosif
We study programs with integer data, procedure calls and arbitrary call graphs. We show that, whenever the guards and updates are given by octagonal relations, the reachability pro…
cs.LO2014
Deciding Entailments in Inductive Separation Logic with Tree Automata
Radu Iosif, Adam Rogalewicz, Tomas Vojnar
Separation Logic (SL) with inductive definitions is a natural formalism for specifying complex recursive data structures, used in compositional verification of programs manipulatin…