Advertisement

Perentie: Modular Trace Refinement and Selective Value Tracking

(Competition Contribution)
  • Franck Cassez
  • Takashi Matsuoka
  • Edward Pierzchalski
  • Nathan Smyth
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)

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.

References

  1. 1.
    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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Franck Cassez
    • 1
    • 2
  • Takashi Matsuoka
    • 1
  • Edward Pierzchalski
    • 1
  • Nathan Smyth
    • 1
  1. 1.NICTASydneyAustralia
  2. 2.Macquarie University and UNSWSydneyAustralia

Personalised recommendations