P. Cousot, Program Unrolling by Abstract Interpretation for Probabilistic Proofs

Patrick Cousot.
Program Unrolling by Abstract Interpretation for Probabilistic Proofs.
In DARPA SIEVE project, Computer Science, New York University, June 2021.
Paper (38 pages): PDF (217 KB)

Abstract: Probabilistic proofs require to unroll programs loops and functions. This is a great opportunity for static analysis since unbounded loops and unrestricted recursion can only be handled by induction or coinduction, which in those static analyses using the more powerful infinitary abstract domains require the use of extrapolation operators (widenings and their duals) and interpolation operators (narrowings and their dual) which are weak mechanizable forms of induction and coinduction, at the origin of losses of information during static analysis. We formalize the simultaneous static analysis and program unrolling and proved the soundness of the approach by abstraction of a programming language labelled trace semantics
Keywords: Abstract interpretation, Static analysis, Optimization, Unrolling.

\bibitem{CousotSieve21}
Patrick Cousot.
\newblock Program Unrolling by Abstract Interpretation for Probabilistic Proofs.
\newblock Computer Science, New York University,
  38 pages, June 2021.

@techreport{CousotSieve21
   author =      {Patrick Cousot},
   title =       {Program Unrolling by Abstract Interpretation for 
                  Probabilistic Proofs},
   pages =       {38},
   institution = {Computer Science, New York University},
   month =       {June},
   year =        2021,
 }

copyright notice
Last modified: Saturday, 26-June-2021 11:08:22 EST