2 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.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.…