×

Extracting program logics from abstract interpretations defined by logical relations. (English) Zbl 1316.68042

Fiore, Marcelo (ed.), Proceedings of the 23rd conference on the mathematical foundations of programming semantics (MFPS XXIII), New Orleans, LA, USA, April 11–14, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 173, 339-356 (2007).
Summary: We connect the activity of defining an abstract-interpretation-based static analysis with synthesizing its appropriate programming logic by applying logical relations as demonstrated by Abramsky. We begin with approximation relations of base type, which relate concrete computational values to their approximations, and we lift the relations to function space and upper- and lower-powerset. The resulting family’s properties let us synthesize an appropriate logic for reasoning about the outcome of a static analysis. The relations need not generate Galois connections, but when they do, we show that the relational notions of soundness and completeness coincide with the Galois-connection-based notions.
For the entire collection see [Zbl 1273.68031].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B44 Temporal logic
03B70 Logic in computer science
06A15 Galois correspondences, closure operators (in relation to ordered sets)

Software:

Octagon
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Abramsky, S., Abstract interpretation, logical relations, and kan extensions, J. logic and computation, 1, 5-41, (1990) · Zbl 0727.03020
[2] Abramsky, S., Domain theory in logical form, Ann.pure appl.logic, 51, 1-77, (1991) · Zbl 0737.03006
[3] Baader, F., The description logic handbook, (2003), Cambridge Univ. Press
[4] Backhouse, K.; Backhouse, R., Galois connections and logical relations, () · Zbl 1073.68570
[5] Clarke, E.M.; Grumberg, O.; Peled, D.A., Model checking, (2000), MIT Press
[6] Cleaveland, R.; Iyer, P.; Yankelevich, D., Optimality in abstractions of model checking, ()
[7] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs, (), 238-252 · Zbl 0788.68094
[8] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (), 269-282 · Zbl 0788.68094
[9] Cousot, P.; Cousot, R., Abstract interpretation frameworks, J. logic and computation, 2, 511-547, (1992) · Zbl 0783.68073
[10] Cousot, P.; Cousot, R., Higher-order abstract interpretation, () · Zbl 1323.68367
[11] Cousot, P.; Cousot, R., Temporal abstract interpretation, (), 12-25 · Zbl 1323.68367
[12] D. Dams. Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands, 1996. · Zbl 0848.68060
[13] Dams, D.; Gerth, R.; Grumberg, O., Abstract interpretation of reactive systems, ACM trans. prog. lang. systems, 19, 253-291, (1997)
[14] Giacobazzi, R.; Quintarelli, E., Incompleteness, counterexamples, and refinements in abstract model checking, (), 356-373 · Zbl 1005.68099
[15] Giacobazzi, R.; Ranzato, F.; Scozzari, F., Making abstract interpretations complete, J. ACM, 47, 361-416, (2000) · Zbl 1133.68370
[16] Harel, D.; Kozen, D.; Tiuryn, J., Dynamic logic, (2000), MIT Press · Zbl 0976.68108
[17] Hartmanis, J.; Stearns, R.E., Pair algebras and their application to automata theory, J. information and control, 7, 485-507, (1964) · Zbl 0197.43604
[18] Hennessy, M.C.B.; Milner, Robin, Algebraic laws for non-determinism and concurrency, Jacm, 32, 137-161, (1985) · Zbl 0629.68021
[19] T. Jensen, Abstract Interpretation in Logical Form. PhD thesis, Imperial College, London, 1992.
[20] Jones, N.; Nielson, F., Abstract interpretation: a semantics-based tool for program analysis, (), 527-636
[21] Lacey, D.; Jones, N.D.; VanWyk, E.; Frederiksen, C.C., Compiler optimization correctness by temporal logic, J. higher order and symbolic comp., 17, 173-206, (2004) · Zbl 1075.68015
[22] Loiseaux, C.; Graf, S.; Sifakis, J.; Bouajjani, A.; Bensalem, S., Property preserving abstractions for verification of concurrent systems, Formal methods in system design, 6, 1-36, (1995) · Zbl 0829.68053
[23] MinĂ©, A., The octagon abstract domain, J. higher-order and symbolic computation, 19, 31-100, (2006) · Zbl 1105.68069
[24] Mycroft, A.; Jones, N.D., A relational framework for abstract interpretation, (), 156-171
[25] Nielson, F., Two-level semantics and abstract interpretation, Theoretical computer science, 69, 2, 117-242, (1989) · Zbl 0696.68093
[26] Nielson, F.; Nielson, H.R.; Hankin, C., Principles of program analysis, (1999), Springer Verlag · Zbl 0932.68013
[27] Plotkin, G., Domains, () · Zbl 0809.68085
[28] Plotkin, G.D., Lambda-definability in the full type hierarchy, (), 363-374
[29] Ranzato, F.; Tapparo, F., Strong preservation as completeness in abstract interpretation, (), 18-32 · Zbl 1126.68485
[30] Ranzato, F.; Tapparo, F., Strong preservation of temporal fixpoint-based operators by abstract interpretation, (), 332-347 · Zbl 1176.68127
[31] Schmidt, D.A., Data-flow analysis is model checking of abstract interpretations, ()
[32] Schmidt, D.A., Structure-preserving binary relations for program abstraction, (), 246-266
[33] Schmidt, D.A., Closed and logical relations for over- and under-approximation of powersets, (), 22-37 · Zbl 1104.68024
[34] Schmidt, D.A., Comparing completeness properties of static analyses and their logics, (), 183-199 · Zbl 1168.68364
[35] Schmidt, D.A., Underapproximating predicate transformers, (), 127-143 · Zbl 1225.68078
[36] Schmidt, D.A., A calculus of logical relations for over- and underapproximating static analyses, Science comp. programming, 64, 29-53, (2007) · Zbl 1171.68543
[37] Schmidt, D.A.; Steffen, B., Data-flow analysis as model checking of abstract interpretations, ()
[38] Shmuely, Z., The structure of Galois connections, Pacific J. mathematics, 54, 209-225, (1974) · Zbl 0275.06003
[39] Smyth, M., Powerdomains, Journal of computer and system sciences, 16, 23-36, (1978) · Zbl 0408.68017
[40] Steffen, B., Generating data-flow analysis algorithms for modal specifications, Science of computer programming, 21, 115-139, (1993) · Zbl 0815.68070
[41] Venet, A., Automatic determination of communication topologies in mobile systems, (), 152-167
[42] Winskel, G., On powerdomains and modality, Theor. comput. sci., 36, 127-137, (1985) · Zbl 0579.68018
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.