Abstract
We present a static correlation analysis that computes a safe approximation of what part of an input state of a function is copied to the output state. This information is to be used by an interactive theorem prover to automate the discharging of proof obligations concerning unmodified parts of the state. The analysis is defined for a strongly-typed, functional language that handles structures, variants and arrays. It uses partial equivalence relations as approximations of fine-grained correlations between inputs and outputs. The analysis is interprocedural and summarizes not only what is modified but also how and to what extent. We have applied it to a functional specification of a micro-kernel, and obtained results that demonstrate both its precision and its scalability.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
References
Andreescu, O.F., Jensen, T., Lescuyer, S.: Dependency analysis of functional specifications with algebraic data structures. In: Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Proceedings, pp. 116–133 (2015). doi:10.1007/978-3-319-25423-4_8
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of Bi-abduction. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 289–300 (2009). http://doi.acm.org/10.1145/1480881.1480917
Chang, B.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Proceedings, pp. 147–163 (2005). http://dx.doi.org/10.1007/978-3-540-30579-8_11
Jones, N.D., Muchnick, S.S.: Flow analysis and optimization of lisp-like structures. In: Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, 1979, pp. 244–256 (1979). http://doi.acm.org/10.1145/567752.567776
Kildall, G.A.: A unified approach to global program optimization. In: Conference Record of the ACM Symposium on Principles of Programming Languages, 1973, pp. 194–206 (1973). http://doi.acm.org/10.1145/512927.512945
Lattner, C., Lenharth, A., Adve, V.S.: Making context-sensitive points-to analysis with heap cloning practical for the real world. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007, pp. 278–289 (2007). http://doi.acm.org/10.1145/1250734.1250766
Lescuyer, S.: ProvenCore: towards a verified isolation micro-kernel (2015). http://milsworkshop2015.euromils.eu/downloads/hipeac_literature/04-mils15_submission_6.pdf
Mccarthy, J., Hayes, P.J.: Some philosophical problems from the standpoint of artificial intelligence. In: Machine Intelligence. Edinburgh University Press (1969)
Meyer, B.: Framing the frame problem. In: Dependable Software Systems Engineering, pp. 193–203 (2015). http://dx.doi.org/10.3233/978-1-61499-495-4-193
Milanova, A., Rountev, A., Ryder, B.G.: Parameterized object sensitivity for points-to analysis for Java. ACM Trans. Softw. Eng. Methodol. 14(1), 1–41. http://doi.acm.org/10.1145/1044834.1044835 (2005)
Montenegro, M., Peña, R., Segura, C.: Shape analysis in a functional language by using regular languages. Sci. Comput. Program. 111, 51–78 (2015). http://dx.doi.org/10.1016/j.scico.2014.12.006
Rakamaric, Z., Hu, A.J.: Automatic inference of frame axioms using static analysis. In: 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), pp. 89–98 (2008). http://dx.doi.org/10.1109/ASE.2008.19
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL 1999, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1999, pp. 105–118 (1999). http://doi.acm.org/10.1145/292540.292552
Sălcianu, A., Rinard, M.: Purity and side effect analysis for Java programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 199–215. Springer, Heidelberg (2005)
Taghdiri, M., Seater, R., Jackson, D.: Lightweight extraction of syntactic specifications. In: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, pp. 276–286 (2006). http://doi.acm.org/10.1145/1181775.1181809
Acknowledgments
We would like to thank the anonymous referees for helpful comments and suggestions. For their excellent comments and sharp observations, we are particularly grateful to Olivier Delande and Georges Dupéron. Our article also benefited from the remarks of B. Montagu and H. Chataing.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Andreescu, O.F., Jensen, T., Lescuyer, S. (2016). Correlating Structured Inputs and Outputs in Functional Specifications. In: De Nicola, R., Kühn, E. (eds) Software Engineering and Formal Methods. SEFM 2016. Lecture Notes in Computer Science(), vol 9763. Springer, Cham. https://doi.org/10.1007/978-3-319-41591-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-41591-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41590-1
Online ISBN: 978-3-319-41591-8
eBook Packages: Computer ScienceComputer Science (R0)