3 papers
cs.LO2004
Incompleteness of States w.r.t. Traces in Model Checking
Roberto Giacobazzi, Francesco Ranzato
Cousot and Cousot introduced and studied a general past/future-time specification language, called mu*-calculus, featuring a natural time-symmetric trace-based semantics. The stand…
cs.LO2004
Generalized Strong Preservation by Abstract Interpretation
Francesco Ranzato, Francesco Tapparo
Standard abstract model checking relies on abstract Kripke structures which approximate concrete models by gluing together indistinguishable states, namely by a partition of the co…
cs.PL2002
Making Abstract Domains Condensing
R. Giacobazzi, F. Ranzato, F. Scozzari
In this paper we show that reversible analysis of logic languages by abstract interpretation can be performed without loss of precision by systematically refining abstract domains.…