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