|
|
|
|
Список литературы
|
|
| |
| 1. |
G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, G. Heiser, “Comprehensive formal verification of an os microkernel”, ACM Transactions on Computer Systems, 32:1 (2014), 2:1-2:70   |
| 2. |
T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani, A. Ustuner, “Thorough static analysis of device drivers”, SIGOPS Operating Systems Review, 40:4 (2006), 73-85 |
| 3. |
D. Engler, M. Musuvathi, “Static analysis versus software model checking for bug finding”, Lecture Notes in Computer Science, 2937, 2004, 191-210 |
| 4. |
Saturn. Precise and Scalable Software Analysis: http://saturn.stanford.edu/ (accessed 01.12.2018) |
| 5. |
T. Witkowski, N. Blanc, D. Kroening, G. Weissenbacher, “Model checking concurrent Linux device drivers”, Proceedings of the 22nd IEEE/ACM Int. Conference on Automated Software Engineering, 2007, 501-504 |
| 6. |
N. Palix, G. Thomas, S. Saha, C. Calvès, J. Lawall, G. Muller, “Faults in Linux: Ten years later”, Proceedings of the 16th Int. Conference on Architectural Support for Programming Languages and Operating Systems, 2011, 305-318 |
| 7. |
Linux driver verification project: http://linuxtesting.org/ldv (accessed 01.12.2018) |
| 8. |
В. С. Мутилин, Е. М. Новиков, А. В. Хорошилов, “Анализ типовых ошибок в драйверах операционной системы Linux”, Труды ИСП РАН, 22 (2012), 349-374 [V. Mutilin, E. Novikov, A. Khoroshilov, “Analysis of typical faults in Linux operating system drivers”, Proc. ISP RAS, 22 (2012), 349-374 (in Russian)] |
| 9. |
A. Khoroshilov, V. Mutilin, A. Petrenko, V. Zakharov, “Establishing Linux driver verification process”, Lecture Notes in Computer Science, 5947, 2010, 165-176 |
| 10. |
I. Zakharov, M. Mandrykin, V. Mutilin, E. Novikov, A. Petrenko, A. Khoroshilov, “Configurable toolset for static verification of operating systems kernel modules”, Programming and Computer Software, 41:1 (2015), 49-64  |
| 11. |
Klever verification framework: https://forge.ispras.ru/projects/klever (accessed 01.12.2018) |
| 12. |
I. S. Zakharov, V. S. Mutilin, A. V. Khoroshilov, “Pattern-based environment modeling for static verification of linux kernel modules”, Programming and Computer Software, 41:3 (2015), 183-195 |
| 13. |
A. Khoroshilov, V. Mutilin, E. Novikov, I. Zakharov, “Modeling environment for static verification of linux kernel modules”, Lecture Notes in Computer Science, 8974, 2015, 400-414  |
| 14. |
E. Novikov, I. Zakharov, “Towards automated static verification of GNU C programs”, Lecture Notes in Computer Science, 10742, 2018, 402-416 |
| 15. |
D. Beyer, M. Keremoglu, “CPAchecker: A tool for configurable software verification”, Lecture Notes in Computer Science, 6806, 2011, 184-190 |
| 16. |
K. Dudka, P. Peringer, T. Vojnar, “Byte-precise verification of low-level list manipulation”, Lecture Notes in Computer Science, 7935, 2013, 215-237 |
| 17. |
R. Wilhelm, S. Sagiv, T. W. Reps, “Shape analysis”, Lecture Notes in Computer Science, 1781, 2000, 1-17 |
| 18. |
D. Beyer, T. A. Henzinger, G. Théoduloz, “Configurable software verification: concretizing the convergence of model checking and program analysis”, Lecture Notes in Computer Science, 4590, 2007, 504-518 |
