Amrollahi, D., Bartocci, E., Kenison, G., Kovacs, L., Moosbrugger, M., & Stankovič, M. (2024). Correction: (Un)Solvable loop analysis. Formal Methods in System Design. https://doi.org/10.1007/s10703-024-00465-y
(note to production team) please include the relevant hyperlinks to Examples 36, 37, and 38 as appropriate. Further examples of trace maps (Examples 37 and 38 below) are constructed from similar substitution rules on strings of matrices. For Examples 37–38, our work generates the cubic polynomial invariant (Formula presented.) from the well-studied class of Fricke–Vogt invariants as well as higher-degree polynomial invariants. Further examples of trace maps (Examples 37 and 38 below) are constructed from similar substitution rules on strings of matrices. Let (Formula presented.) Then our work generates the cubic polynomial invariants I<inf>1</inf>(x,y,z)-I<inf>1</inf>(x<inf>0</inf>,y<inf>0</inf>,z<inf>0</inf>)=0, I<inf>2</inf>(x,y,z)-I<inf>2</inf>(x<inf>0</inf>,y<inf>0</inf>,z<inf>0</inf>)=0, and I<inf>3</inf>(x,y,z)-I<inf>3</inf>(x<inf>0</inf>,y<inf>0</inf>,z<inf>0</inf>)=0 for Example 36, Example 37, and Example 38, respectively. The original article has been corrected.
-
Project title:
Distribution Recovery for Invariant Generation of Probabilistic Programs: ICT19-018 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
-
Research Areas:
Computer Engineering and Software-Intensive Systems: 100%
