References

  1. Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg & Pierre-Yves Strub (2017): A Relational Logic for Higher-Order Programs. In: ICFP, doi:10.1145/3110265.
  2. Aws Albarghouthi & Kenneth L. McMillan (2013): Beautiful Interpolants. In: CAV, doi:10.1007/978-3-642-39799-8_22.
  3. David A. Naumann Anindya Banerjee & Mohammad Nikouei (2016): Relational Logic with Framing and Hypotheses. In: FSTTCS, doi:10.4230/LIPIcs.FSTTCS.2016.11.
  4. John D. Backes, Suzette Person, Neha Rungta & Oksana Tkachuk (2013): Regression Verification Using Impact Summaries. In: SPIN, doi:10.1007/978-3-642-39176-7_7.
  5. Gilles Barthe, Juan Manuel Crespo & César Kunz (2011): Relational Verification Using Product Programs. In: FM, doi:10.1007/978-3-642-21437-0_17.
  6. Gilles Barthe, Juan Manuel Crespo & César Kunz (2013): Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. In: LNCS, doi:10.1007/978-3-642-35722-0_3.
  7. Gilles Barthe, Juan Manuel Crespo & César Kunz (2016): Product Programs and Relational Program Logics. In: JLAMP, doi:10.1016/j.jlamp.2016.05.004.
  8. Gilles Barthe, Pedro R. D'Argenio & Tamara Rezk (2004): Secure Information Flow by Self-Composition. In: CSFW-17, doi:10.1017/S0960129511000193.
  9. Lennart Beringer (2011): Relational Decomposition. In: ITP, doi:10.1007/978-3-642-22863-6_6.
  10. Nikolaj Bjørner, Kenneth L. McMillan & Andrey Rybalchenko (2013): On Solving Universally Quantified Horn Clauses. In: SAS, doi:10.1007/978-3-642-38856-9_8.
  11. Marcel Böhme, Bruno C. d. S. Oliveira & Abhik Roychoudhury (2013): Partition-based regression verification. In: ICSE, doi:10.1109/ICSE.2013.6606576.
  12. Alberto Pettorossi Emanuele De Angelis, Fabio Fioravanti & Maurizio Proietti (2016): Verifying Relational Program Properties by Transforming Constrained Horn Clauses. In: CILC.
  13. Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer & Mattias Ulbrich (2014): Automating regression verification. In: ASE, doi:10.1145/2642937.2642987.
  14. Benny Godlin & Ofer Strichman (2009): Regression verification. In: DAC, doi:10.1145/1629911.1630034.
  15. Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri & Henrique Rebêlo (2013): Towards Modularly Comparing Programs Using Automated Theorem Provers. In: CADE-24, doi:10.1007/978-3-642-38574-2_20.
  16. (2016): LeetCode Online Judge. https://leetcode.com/. Accessed: 2015 Nov 16.
  17. Nuno P. Lopes & José Monteiro (2016): Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. STTT 18(4), doi:10.1007/s10009-015-0366-1.
  18. Mattias Ulbrich Moritz Kiefer, Vladimir Klevanov (2016): Relational Program Reasoning Using Compiler IR. In: VSTTE, doi:10.1007/s10817-017-9433-5.
  19. Lauren Pick, Grigory Fedyukovich & Aartic Gupta (2018): Exploiting Synchrony and Symmetry in Relational Verification. In: CAV, doi:10.1007/978-3-319-96145-3_9.
  20. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg & Brent Yorgey (2018): Logical Foundations. Software Foundations series, volume 1. Electronic textbook. Version 5.5. http://www.cis.upenn.edu/~bcpierce/sf.
  21. Marcelo Sousa & Isil Dillig (2016): Cartesian Hoare logic for verifying k-safety properties. In: PLDI, doi:10.1145/2980983.2908092.
  22. Tachio Terauchi & Alexander Aiken (2005): Secure Information Flow as a Safety Problem. In: SAS, doi:10.1007/11547662_24.
  23. Hiroshi Unno & Sho Torii (2017): Automating Induction for Solving Horn Clauses. In: CAV, doi:10.1007/978-3-319-63390-9_30.
  24. (2017): Z3Prover/z3 - GitHub. https://github.com/Z3Prover/z3. Accessed: 2017 July 1.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org