Использование инвариантов функции высокого уровня для дедуктивной верификации машинного кода
https://doi.org/10.15514/ISPRAS-2019-31(3)-10
Аннотация
Об авторе
Павел Андреевич ПутроРоссия
Список литературы
1. . R.W. Floyd. Assigning Meanings to Programs. Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, 19, 1967. P. 19-32. DOI: 10.1090/psapm/019/0235771.
2. . C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10), 1969. P. 576-585. DOI: 10.1145/363235.363259.
3. . C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Satisfiability Modulo Theories. Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, (A. Biere, M. J. H. Heule, H. van Maaren, and T. Walsh, eds.), IOS Press, Feb. 2009, pp. 825885.
4. . C. Sun, V. Le, Q. Zhang, Z. Su Toward understanding compiler bugs in gcc and llvm. ISSTA 2016, pp. 294-305.
5. . Putro P.A. Combining ACSL Specifications and Machine Code. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 4, 2018. pp. 95-106. DOI: 10.15514/ISPRAS-2018-30(4)-6
6. . M.O. Myreen. Formal Verification of Machine-Code Programs. Ph.D. Thesis. University of Cambridge, 2009. 131 p.
7. . K. Slind, M. Norrish. A Brief Overview of HOL4. Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science (LNCS), 5170, 2008. P. 28-32. DOI: 10.1007/978-3-540-71067-7 6.
8. . A. Fox. Formal Specification and Verification of ARM6. Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science (LNCS), 2758, 2003. P. 25-40. DOI: 10.1007/10930755 2.
9. . K. Crary, S. Sarkar. Foundational Certified Code in a Metalogical Framework. Technical Report CMU-CS-03-108. Carnegie Mellon University, 2003. 19 p.
10. . X. Leroy. Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant. Principles of Programming Languages (POPL), 2006. P. 42-54, DOI: 10.1145/1111037.1111042.
11. . Y. Bertot. A Short Presentation of Coq. Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science, 5170, 2008. P. 12-16. DOI: 10.1007/978-3-540-71067-7 3.
12. . P. Baudin, P. Cuoq, J.-C. Filliˆatre, C. March´e, B. Monate, Y. Moy, V. Prevosto. ACSL: ANSI/ISO C Specification Language. Version 1.13, 2018. 114 p.
13. . T.M.T. Nguyen, C. March´e. Hardware-Dependent Proofs of Numerical Programs. Certified Programs and Proofs (CPP), 2011. Lecture Notes in Computer Science 7086. P. 314-329. DOI: 10.1007/978-3-642-25379-9 23.
14. . G. Barthe, T. Rezk, A. Saabas. Proof Obligations Preserving Compilation. Formal Aspects in Security and Trust (FAST), 2005. Lecture Notes in Computer Science 3866. P. 112-126. DOI: 10.1007/11679219 9.
15. . MicroTESK Framework – http://www.microtesk.org
16. . M. Freericks. The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department, 1993. 47 p.
17. . C. Barrett, P. Fontaine, C. Tinelli. The SMT-LIB Standard Version 2.6. Release 2017-07-18. 104 p.
18. . JavaScript Object Notation – https://www.json.org/
19. . R. E. Tarjan, Dep-first search and linear graph algorithms SIAM J. Comput., vol. 1, no. 2, pp. 146-160, June 1972.
20. . ocaml-containers library – https://github.com/c-cube/ocaml-containers
Рецензия
Для цитирования:
Путро П.А. Использование инвариантов функции высокого уровня для дедуктивной верификации машинного кода. Труды Института системного программирования РАН. 2019;31(3):123-134. https://doi.org/10.15514/ISPRAS-2019-31(3)-10
For citation:
Putro P.A. Applying High-Level Function Loop Invariants for Machine Code Deductive Verification. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(3):123-134. https://doi.org/10.15514/ISPRAS-2019-31(3)-10