Abstract
Perentie is a software analysis tool based on iterative refinement of trace abstraction: if the refinement process terminates, the program is either declared correct or a counterexample is provided and the program is incorrect.
Chapter PDF
Similar content being viewed by others
References
Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69–85. Springer, Heidelberg (2009)
Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013)
Cassez, F., Müller, C., Burnett, K.: Summary-based inter-procedural analysis via modular trace refinement. In: FSTTCS 2014, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, New Dehli, India, December 15-17, vol. 29, pp. 545–556 (2014)
Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An Interpolating SMT Solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cassez, F., Matsuoka, T., Pierzchalski, E., Smyth, N. (2015). Perentie: Modular Trace Refinement and Selective Value Tracking. In: Baier, C., Tinelli, C. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2015. Lecture Notes in Computer Science(), vol 9035. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_39
Download citation
DOI: https://doi.org/10.1007/978-3-662-46681-0_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46680-3
Online ISBN: 978-3-662-46681-0
eBook Packages: Computer ScienceComputer Science (R0)