Effective Automated Software Verification: A Multilayered Approach

• Název práce v češtině: Efektivní automatická verifikace software: Vícevrstvý přístup
• Název v anglickém jazyce: Effective Automated Software Verification: A Multilayered Approach
• Klíčová slova: automatická verifikace software|formální verifikace|model checking|Hornovy klauzule s omezujícími podmínkami|Craigova interpolace|SMT
• Klíčová slova anglicky: automated verification of software|formal verification|model checking|constrained Horn clauses|Craig interpolation|SMT
• Akademický rok vypsání: 2016/2017
• Typ práce: disertační práce
• Jazyk práce: angličtina
• Ústav: Katedra distribuovaných a spolehlivých systémů (32-KDSS)
• Vedoucí / školitel: doc. RNDr. Jan Kofroň, Ph.D.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 03.10.2016
• Datum zadání: 03.10.2016
• Datum potvrzení stud. oddělením: 04.10.2016
• Datum a čas obhajoby: 21.03.2023 08:15
• Datum odevzdání elektronické podoby: 25.01.2023
• Datum odevzdání tištěné podoby: 26.01.2023
• Datum proběhlé obhajoby: 21.03.2023
• Oponenti: prof. Philipp Rümmer

Zásady pro vypracování

Software verification is a field undergoing vast development. This is because the computer systems penetrate everyday lives in a more and more frequent and deeper way, being required to satisfy safety properties in many cases.

The goal of this thesis is to push further the limits of automated software verification by means of symbolic methods, widening thus the set of programs that can be verified. In particular, the work should focus on research in the area of Craig Interpolants, where the goals include developing algorithms for faster construction of interpolants as well as reducing their size. These aspects currently represent the bottlenecks in verification in general, and in software verification in particular.

Seznam odborné literatury

1. A. Albarghouthi, A. Gurfinkel, and M. Chechik. From Under-Approximations to OverApproximations and Back. In TACAS, pages 157–172, 2012.
2. O. Bar-Ilan, O. Fuhrmann, S. Hoory, O. Shacham, and O. Strichman. Linear-Time Reductions of Resolution Proofs. In HVC, pages 114–128, 2008.
3. J. Boudou, A. Fellner, and B. W. Paleo. Skeptik: A Proof Compression System. In IJCAR, pages 374–380, 2014.
4. J. Boudou and B. W. Paleo. Compression of propositional resolution proofs by lowering subproofs. In TABLEAUX, pages 59–73, 2013.
5. G. Cabodi, C. Loiacono, and D. Vendraminetto. Optimization Techniques for Craig Interpolant Compaction in Unbounded Model Checking. In DATE, pages 1417–1422, 2013.
6. S. Cotton. Two Techniques for Minimizing Resolution Proofs. In SAT, pages 306–312, 2010.
7. W. Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Symbolic Logic, pages 269–285, 1957.
8. V. D’Silva, D. Kroening, M. Purandare, and G. Weissenbacher. Interpolant Strength. In VMCAI, pages 129–145, 2010.
9. N. Eén and A. Biere. Effective Preprocessing in SAT Through Variable and Clause Elimination. In SAT, pages 61–75, 2005.
10. G. Fedyukovich, O. Sery, and N. Sharygina. eVolCheck: Incremental upgrade checker for C. In TACAS, pages 292–307, 2013.
11. P. Fontaine, S. Merz, and B. W. Paleo. Compression of Propositional Resolution Proofs via Partial Regularization. In CADE-23, pages 237–251, 2011.
12. P. Jancik, J. Kofron, S. F. Rollini, and N. Sharygina. On Interpolants and Variable Assignments. In FMCAD, pages 123–130, 2014.
13. R. Jhala and K. L. McMillan. A Practical and Complete Approach to Predicate Refinement. In H. Hermanns and J. Palsberg, editors, TACAS 2006, volume 3920 of Lecture Notes in Computer Science, pages 459–473. Springer, 2006.
14. A. Kuehlmann, M. K. Ganai, and V. Paruthi. Circuit-based Boolean Reasoning. In DAC, pages 232–237, 2001.
15. K. L. McMillan. Interpolation and SAT-Based Model Checking. In CAV, pages 1–13, 2003.
16. K. L. McMillan. An Interpolating Theorem Prover. In TACAS, pages 16–30, 2004.
17. P. Pudlák. Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Symbolic Logic, pages 981–998, 1997.
18. S. F. Rollini, L. Alt, G. Fedyukovich, A. E. J. Hyvärinen, and N. Sharygina. PeRIPLO: A Framework for Producing Effective Interpolant-based Software Verification. In LPAR, pages 683–693, 2013.
19. S. F. Rollini, R. Bruttomesso, N. Sharygina, and A. Tsitovich. Resolution Proof Transformation for Compression and Interpolation. Formal Methods in System Design, pages 1–41, 2014.
20. S. F. Rollini, O. Sery, and N. Sharygina. Leveraging Interpolant Strength in Model Checking. In CAV, pages 193–209, 2012.
21. O. Sery, G. Fedyukovich, and N. Sharygina. Interpolation-based Function Summaries in Bounded Model Checking. In HVC, pages 160–175, 2011.
22. O. Sery, G. Fedyukovich, and N. Sharygina. FunFrog: Bounded model checking with interpolation-based function summarization. In ATVA, pages 203–207, 2012.
23. O. Sery, G. Fedyukovich, and N. Sharygina. Incremental upgrade checking by means of interpolation-based function summaries. In FMCAD, pages 114–121, 2012.
24. O. Tange. GNU Parallel – The Command-Line Power Tool. The USENIX Magazine, pages 42–47, 2011.
25. G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus. In Studies in Constructive Mathematics and Mathematical Logic, 1969.