Abstract
We describe the Aligator.jl software package for automatically generating all polynomial invariants of the rich class of extended P-solvable loops with nested conditionals. Aligator.jl is written in the programming language Julia and is open-source. Aligator.jl transforms program loops into a system of algebraic recurrences and implements techniques from symbolic computation to solve recurrences, derive closed form solutions of loop variables and infer the ideal of polynomial invariants by variable elimination based on Gröbner basis computation.
All authors are supported by the ERC Starting Grant 2014 SYMCAR 639270. We also acknowledge funding from the Wallenberg Academy Fellowship 2014 TheProSE, the Swedish VR grant GenPro D0497701, and the Austrian FWF research projects RiSE S11409-N23 and W1255-N23. Maximilian Jaroschek is also supported by the FWF project Y464-N18.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Decker, W., Greuel, G.M., Pfister, G., Schönemann, H.: Singular 4-1-0—a computer algebra system for polynomial computations (2016). http://www.singular.uni-kl.de
Humenberger, A., Jaroschek, M., Kovács, L.: Invariant generation for multi-path loops with polynomial assignments. In: Dillig, I., Palsberg, J. (eds.) VMCAI. LNCS, vol. 10747, pp. 226–246. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73721-8_11
Julia. https://julialang.org/
Kovács, L.: Aligator: a mathematica package for invariant generation (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 275–282. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_22
Meurer, A., Smith, C.P., Paprocki, M., Čertík, O., Kirpichev, S.B., Rocklin, M., Kumar, A., Ivanov, S., Moore, J.K., Singh, S., Rathnayake, T., Vig, S., Granger, B.E., Muller, R.P., Bonazzi, F., Gupta, H., Vats, S., Johansson, F., Pedregosa, F., Curry, M.J., Terrel, A.R., Roučka, S., Saboo, A., Fernando, I., Kulal, S., Cimrman, R., Scopatz, A.: SymPy: symbolic computing in Python. PeerJ Comput. Sci. 3, e103 (2017). https://doi.org/10.7717/peerj-cs.103
Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. 42(4), 443–476 (2007). https://doi.org/10.1016/j.jsc.2007.01.002
SageMath. http://www.sagemath.org/
Wolfram, S.: An Elementary Introduction to the Wolfram Language. Wolfram Media Inc. (2017). https://www.wolfram.com/language/elementary-introduction/2nd-ed/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Humenberger, A., Jaroschek, M., Kovács, L. (2018). Aligator.jl – A Julia Package for Loop Invariant Generation. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics. CICM 2018. Lecture Notes in Computer Science(), vol 11006. Springer, Cham. https://doi.org/10.1007/978-3-319-96812-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-96812-4_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-96811-7
Online ISBN: 978-3-319-96812-4
eBook Packages: Computer ScienceComputer Science (R0)