Abstract Interpretations in the Framework of Invariant Sets

• Autorzy: Alexandru A. , Ciobanu G.

Identyfikatory

DOI

10.3233/FI-2016-1321

• Języki publikacji: EN

Abstrakty

EN

We present a theory of abstract interpretations in the framework of invariant sets by translating the notions of lattices and Galois connections into this framework, and presenting their properties in terms of finitely supported objects. We introduce the notions of invariant correctness relation and invariant representation function, emphasize an equivalence between them, and establish the relationship between these notions and invariant Galois connections. Finally, we provide some widening and narrowing techniques in order to approximate the least fixed points of finitely supported transition functions.

Słowa kluczowe

EN

invariant sets; finitely supported object; invariant Galois connection; abstract analysis

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 144, nr 1
• Strony: 1--22
• Opis fizyczny: Bibliogr. 25 poz.

Twórcy

autor

Alexandru A.

• Romanian Academy, Institute of Computer Science Iaşi, Romania

autor

Ciobanu G.

• Romanian Academy, Institute of Computer Science Iaşi, Romania

Bibliografia

• [1] Abramsky S, Ghica D.R, Murawski A.S, Luke Ong C.H, Stark I.D.B. Nominal games and full abstraction for the nu-calculus. In: 19th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press; 2004. p. 150–159. doi: 10.1109/LICS.2004.1319609.
• [2] Alexandru A, Ciobanu G. Nominal techniques for piI-calculus. Romanian Journal of Information Science and Technology. 2013;16(4):261–286. Available from: http://www.imt.ro/romjist/Volum16/Number16_4/pdf/02-GCiobanu2013.pdf.
• [3] Alexandru A, Ciobanu G. Algebraic properties of generalized multisets. In: 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. IEEE Computer Society Press; 2013. p. 369–377. doi: 10.1109/SYNASC.2013.55.
• [4] Alexandru A, Ciobanu G. A nominal approach for fusion calculus. Romanian Journal of Information Science and Technology. 2014; 17(3):265–288. Available from: http://www.imt.ro/romjist/Volum17/Number17_3/pdf/05-GCiobanu2014.pdf.
• [5] Alexandru A, Ciobanu G. Nominal groups and their homomorphism theorems. Fundamenta Informaticae. 2014; 131(3-4):279–298. doi: 10.3233/FI-2014-1015.
• [6] Alexandru A, Ciobanu G. Mathematics of multisets in the Fraenkel-Mostowski framework. Bulletin Mathematique de la Societe des Sciences Mathematiques de Roumanie. 2015;58/106(1):3–18. Available from: http://ssmr.ro/bulletin/pdf/58-1/articol_1.pdf.
• [7] Alexandru A, Ciobanu G. Defining finitely supported mathematics over sets with atoms. In: 4th International Workshop on Algebraic, Logical, and Algorithmic Methods of System Modeling, Specification and Verification, Volume 1356 of CEUR-WS; 2015. p. 382–395. Available from: http://ceur-ws.org/Vol-1356/paper_93.pdf.
• [8] Bojanczyk M. Modelling Infinite Structures with Atoms. In: 20th Workshop on Logic, Language, Information and Computation, Workshop Proceedings. Volume 8071 of LNCS; 2013. p. 13–28. doi: 10.1007/978-3-642-39992-3_3.
• [9] Bojanczyk M. Nominal Monoids. Theory of Computing Systems. 2013;53(2):194–222. doi: 10.1007/s00224-013-9464-1.
• [10] Bojanczyk M, Braud L, Klin B, Lasota S. Towards nominal computation. In: 39th ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press; 2012. p. 401–412. ISBN: 978-1-4503-1083-3. doi: 10.1145/2103656.2103704.
• [11] Bojanczyk M, Klin B, Lasota S. Automata with group actions. In: 26th IEEE Symposium on Logic in Computer Science, Conference Proceedings. IEEE Computer Society Press; 2011. p. 355–364. ISBN: 978-0-7695-4412-0. doi: 10.1109/LICS.2011.48.
• [12] Bojanczyk M, Klin B, Lasota S, Torunczyk S. Turing machines with atoms. In: 28th IEEE Symposium on Logic in Computer Science, Conference Proceedings. IEEE Computer Society Press; 2013. p. 183–192. doi: 10.1109/LICS.2013.24.
• [13] Bojanczyk M, Torunczyk S. Imperative programming in sets with atoms. In: 32nd Foundations of Software Technology and Theoretical Computer Science Conference. Volume 18 of LIPICS; 2012. p. 4–15. Available from: http://drops.dagstuhl.de/opus/volltexte/2012/3843. doi: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2012.4,
• [14] Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Conference Proceedings. ACM Press; 1977. p. 238–252. doi: 10.1145/512950.512973.
• [15] Cousot P, Cousot R. Systematic design of program analysis frameworks. In: 6th ACM SIGPLANSIGACT Symposiumon Principles of Programming Languages. ACM Press; 1979. p. 269–282. doi: 10.1145/567752.567778.
• [16] Gabbay M.J, Pitts A.M. A new approach to abstract syntax with variable binding. Formal Aspects of Computing. 2001;13(3-5):341–363. doi: 10.1007/s001650200016.
• [17] Howard P, Rubin J.E. Consequences of the Axiom of Choice, Volume 59 of Mathematical Surveys and Monographs. American Mathematical Society; 1998.
• [18] Nielson F, Nielson H, Hankin C. Principles of Program Analysis. Springer; 1999. ISBN: 3540654100.
• [19] Petrisan D. Investigations into Algebra and Topology over Nominal Sets, PhD thesis. University of Leicester; 2011.
• [20] Pitts A.M. Nominal logic, a first order theory of names and binding. Information and Computation. 2003; 186(2):165–193. doi: 10.1016/S0890-5401(03)00138-X.
• [21] Pitts A.M. Alpha-structural recursion and induction. Journal of the ACM. 2006;53(3):459–506. doi: 10.1145/1147954.1147961.
• [22] Pitts A.M. Nominal Sets Names and Symmetry in Computer Science. Cambridge University Press; 2013. ISBN: 9781107017788.
• [23] Shinwell M.R. The Fresh Approach: functional programming with names and binders, PhD thesis. University of Cambridge; 2005.
• [24] Turner D. Nominal Domain Theory for Concurrency, Technical Report 751. University of Cambridge; 2009. Available from: http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-751.pdf.
• [25] Urban C. Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning. 2008;40(4):327–356. doi: 10.1007/s10817-008-9097-2.