Abstrakt. Vi presenterar tekniker för analys av oändliga stat probabilistiska program för att syntetisera probabilistiska invarianter och bevisa nästan säker avslutning. Vår analys är baserad på begreppet (super) martingales från sannolikhetsteori. Först definierar vi begreppet (super) martingales för slingor i probabilistiska program. Därefter presenterar vi användningen av koncentrationen av mätojämlikheter för att med stor sannolikhet begränsa värdena på martingales. Detta gör att vi direkt kan dra slutsatsen probabilistiska gränser för påståenden som involverar programvariablerna. Därefter presenterar vi idén om en super martingale ranking funktion (SMRF) för att bevisa nästan säker avslutande av probabilistiska program. Slutligen utökar vi begränsningsbaserade tekniker för att syntetisera martingales och supermartingale rankingfunktioner för probabilistiska program. Vi presenterar några tillämpningar av vårt tillvägagångssätt för att resonera om invarians och avslutande av små men komplexa probabilistiska program.
En av de första är ranking supermartingales, infördes i REF för att bevisa nästan säker uppsägning.
Probabilistic Program Analysis with Martingales
{'venue': 'CAV', 'journal': None, 'mag_field_of_study': ['Computer Science']}