References

  1. Beatriz Alarcon, Raul Gutierrez, Jose Iborra & Salvador Lucas (2007): Proving Termination of Context-Sensitive Rewriting with MU-TERM. ENTCS 188, pp. 105 – 115, doi:10.1016/j.entcs.2007.05.041.
  2. Martin Avanzini, Christian Sternagel & René Thiemann (2015): Certification of Complexity Proofs using CeTA. In: RTA, LIPIcs 36, pp. 23–39, doi:10.4230/LIPIcs.RTA.2015.23. Available at http://drops.dagstuhl.de/opus/volltexte/2015/5187.
  3. Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano & Peter O'Hearn (2007): Variance Analyses from Invariance Analyses. In: POPL, pp. 211–224, doi:10.1145/1190216.1190249.
  4. Denis Bogdănaş & Grigore Roşu (2015): K-Java: A Complete Semantics of Java. In: POPL, pp. 445–456, doi:10.1145/2676726.2676982.
  5. Marc Brockschmidt, Byron Cook & Carsten Fuhs (2013): Better Termination Proving through Cooperation. In: CAV, pp. 413–429, doi:10.1007/978-3-642-39799-8_28.
  6. Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf & Nir Piterman (2016): T2: Temporal Property Verification. In: TACAS, pp. 387–393, doi:10.1007/978-3-662-49674-9_22.
  7. Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds & Andrew W. Appel (2018): VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. JAR, doi:10.1007/s10817-018-9457-5.
  8. Ştefan Ciobâcă & Dorel Lucanu (2018): A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. In: IJCAR, pp. 295–311, doi:10.1007/978-3-319-94205-6_20.
  9. Ştefan Ciobâcă (2014): Reducing Partial Equivalence to Partial Correctness. In: SYNASC, pp. 164–171, doi:10.1109/SYNASC.2014.30.
  10. Ştefan Ciobâcă & Dorel Lucanu (2016): RMT: Proving Reachability Properties in Constrained Term Rewriting Systems Modulo Theories. Technical Report TR 16-01. Alexandru Ioan Cuza University, Faculty of Computer Science.
  11. Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons & Xavier Urbain (2007): Certification of Automated Termination Proofs. In: FroCoS, pp. 148–162, doi:10.1007/978-3-540-74621-8_10.
  12. Byron Cook, Andreas Podelski & Andrey Rybalchenko (2006): Termination Proofs for Systems Code. In: PLDI, pp. 415–426, doi:10.1145/1133981.1134029.
  13. Byron Cook, Abigail See & Florian Zuleger (2013): Ramsey vs. Lexicographic Termination Proving. In: TACAS, pp. 47–61, doi:10.1007/978-3-642-36742-7_4.
  14. Andrei Ştefănescu, Ştefan Ciobâcă, Radu Mereuţă, Brandon M. Moore, Traian Florin Şerbănuţă & Grigore Roşu (2014): All-Path Reachability Logic. In: RTA-TLCA, pp. 425–440, doi:10.1007/978-3-319-08918-8_29.
  15. Andrei Ştefănescu, Daejun Park, Shijiao Yuwen, Yilong Li & Grigore Roşu (2016): Semantics-Based Program Verifiers for All Languages. In: OOPSLA, pp. 74–91, doi:10.1145/2983990.2984027.
  16. Chucky Ellison & Grigore Roşu (2012): An Executable Formal Semantics of C with Applications. In: POPL, pp. 533–544, doi:10.1145/2103656.2103719.
  17. Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski & René Thiemann (2017): Analyzing Program Termination and Complexity Automatically with AProVE. JAR 58(1), pp. 3–31, doi:10.1007/s10817-016-9388-y.
  18. Dorel Lucanu, Vlad Rusu & Andrei Arusoaie (2017): A generic framework for symbolic execution: a coinductive approach. J. Symb. Comput. 80, pp. 125–163, doi:10.1016/j.jsc.2016.07.012.
  19. Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner & Julian Sutherland (2016): Modular Termination Verification for Non-Blocking Concurrency. In: ESOP, pp. 176–201, doi:10.1007/978-3-662-49498-1_8.
  20. Grigore Roşu & Andrei Ştefănescu (2012): Checking Reachability using Matching Logic. In: OOPSLA, pp. 555–574, doi:10.1145/2384616.2384656.
  21. Grigore Roşu, Andrei Ştefănescu, Ştefan Ciobâcă & Brandon M. Moore (2013): One-Path Reachability Logic. In: LICS, pp. 358–367, doi:10.1109/LICS.2013.42.
  22. Grigore Roşu, Chucky Ellison & Wolfram Schulte (2010): Matching Logic: An Alternative to Hoare/Floyd Logic. In: AMAST, LNCS 6486, pp. 142–162, doi:10.1007/978-3-642-17796-5_9.
  23. Manfred Schmidt-Schauß & David Sabel (2010): Closures of may-, should-and must-convergences for contextual equivalence. Information Processing Letters 110(6), pp. 232–235, doi:10.1016/j.ipl.2010.01.001.
  24. Traian Florin Şerbănuţă, Grigore Roşu & José Meseguer (2009): A Rewriting Logic Approach to Operational Semantics. Information and Computation 207(2), pp. 305–340, doi:10.1016/j.ic.2008.03.026.
  25. Dominic Steinhöfel & Nathan Wasser (2017): A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows. In: iFM, pp. 279–294, doi:10.1007/978-3-319-66845-1_18.
  26. Glynn Winskel (1993): The formal semantics of programming languages. Foundations of Computing.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org