20
D. Beyer and M. Dangl
14. Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M.,
O’Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast
with software verification. In: Proc. NFM. pp. 3–11. LNCS 9058, Springer (2015).
https://doi.org/10.1007/978-3-319-17524-9_1
15. Cimatti, A., Griggio, A.: Software model checking via IC3. In: Proc. CAV. pp. 277–
293. LNCS 7358, Springer (2012). https://doi.org/10.1007/978-3-642-31424-7_23
16. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant
checking with IC3 and predicate abstraction. FMSD 49(3), 190–218 (2016).
https://doi.org/10.1007/s10703-016-0257-4
17. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided
abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003).
https://doi.org/10.1145/876638.876643
18. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb.
Log. 22(3), 250–268 (1957). https://doi.org/10.2307/2963593
19. Graf, S., Saïdi, H.: Construction of abstract state graphs with Pvs. In: Proc. CAV.
pp. 72–83. LNCS 1254, Springer (1997). https://doi.org/10.1007/3-540-63166-6_10
20. Günther, H., Laarman, A., Weissenbacher, G.: Vienna Verification Tool: IC3 for parallel software (competition contribution). In: Proc. TACAS. pp. 954–957. LNCS 9636,
Springer (2016)
21. Gurfinkel, A., Chaki, S.: Boxes: A symbolic abstract domain of boxes. In: Proc.
SAS. pp. 287–303 (2010). https://doi.org/10.1007/978-3-642-15769-1_18
22. Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: A framework for verifying C
programs (competition contribution). In: Proc. TACAS. pp. 447–450. LNCS 9035,
Springer (2015). https://doi.org/10.1007/978-3-662-46681-0_41
23. Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Proc. CAV. pp. 343–361. LNCS 9206, Springer (2015).
https://doi.org/10.1007/978-3-319-21690-4_20
24. Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys 41(4)
(2009). https://doi.org/10.1145/1592434.1592438
25. Jovanovic, D., Dutertre, B.: Property-directed k-induction. In: Proc. FMCAD. pp.
85–92. IEEE (2016). https://doi.org/10.1109/FMCAD.2016.7886665
26. Kahsai, T., Tinelli, C.: PKind: A parallel k-induction based model checker. In:
Proc. Int. Workshop on Parallel and Distributed Methods in Verification. pp. 55–62.
EPTCS 72 (2011). https://doi.org/10.4204/EPTCS.72
27. Khoroshilov, A.V., Mutilin, V.S., Petrenko, A.K., Zakharov, V.: Establishing Linux
driver verification process. In: Proc. Ershov Memorial Conference. pp. 165–176.
LNCS 5947, Springer (2009). https://doi.org/10.1007/978-3-642-11486-1_14
28. Lange, T., Neuhäußer, M.R., Noll, T.: IC3 software model checking on control flow
automata. In: Proc. FMCAD. pp. 97–104 (2015)
29. Lange, T., Prinz, F., Neuhäußer, M.R., Noll, T., Katoen, J.: Improving generalization
in software IC3. In: Proc. SPIN’18. pp. 85–102. LNCS 10869, Springer (2018).
https://doi.org/10.1007/978-3-319-94111-0_5
30. McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. CAV. pp.
1–13. LNCS 2725, Springer (2003). https://doi.org/10.1007/978-3-540-45069-6_1
31. Myers, G.J., Sandler, C., Badgett, T.: The Art of Software Testing. Wiley Publishing,
3rd edn. (2011)
32. Wahl, T.: The k-induction principle (2013), available at http://www.ccs.neu.edu/
home/wahl/Publications/k-induction.pdf
D. Beyer and M. Dangl
14. Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M.,
O’Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast
with software verification. In: Proc. NFM. pp. 3–11. LNCS 9058, Springer (2015).
https://doi.org/10.1007/978-3-319-17524-9_1
15. Cimatti, A., Griggio, A.: Software model checking via IC3. In: Proc. CAV. pp. 277–
293. LNCS 7358, Springer (2012). https://doi.org/10.1007/978-3-642-31424-7_23
16. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant
checking with IC3 and predicate abstraction. FMSD 49(3), 190–218 (2016).
https://doi.org/10.1007/s10703-016-0257-4
17. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided
abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003).
https://doi.org/10.1145/876638.876643
18. Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb.
Log. 22(3), 250–268 (1957). https://doi.org/10.2307/2963593
19. Graf, S., Saïdi, H.: Construction of abstract state graphs with Pvs. In: Proc. CAV.
pp. 72–83. LNCS 1254, Springer (1997). https://doi.org/10.1007/3-540-63166-6_10
20. Günther, H., Laarman, A., Weissenbacher, G.: Vienna Verification Tool: IC3 for parallel software (competition contribution). In: Proc. TACAS. pp. 954–957. LNCS 9636,
Springer (2016)
21. Gurfinkel, A., Chaki, S.: Boxes: A symbolic abstract domain of boxes. In: Proc.
SAS. pp. 287–303 (2010). https://doi.org/10.1007/978-3-642-15769-1_18
22. Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: A framework for verifying C
programs (competition contribution). In: Proc. TACAS. pp. 447–450. LNCS 9035,
Springer (2015). https://doi.org/10.1007/978-3-662-46681-0_41
23. Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Proc. CAV. pp. 343–361. LNCS 9206, Springer (2015).
https://doi.org/10.1007/978-3-319-21690-4_20
24. Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys 41(4)
(2009). https://doi.org/10.1145/1592434.1592438
25. Jovanovic, D., Dutertre, B.: Property-directed k-induction. In: Proc. FMCAD. pp.
85–92. IEEE (2016). https://doi.org/10.1109/FMCAD.2016.7886665
26. Kahsai, T., Tinelli, C.: PKind: A parallel k-induction based model checker. In:
Proc. Int. Workshop on Parallel and Distributed Methods in Verification. pp. 55–62.
EPTCS 72 (2011). https://doi.org/10.4204/EPTCS.72
27. Khoroshilov, A.V., Mutilin, V.S., Petrenko, A.K., Zakharov, V.: Establishing Linux
driver verification process. In: Proc. Ershov Memorial Conference. pp. 165–176.
LNCS 5947, Springer (2009). https://doi.org/10.1007/978-3-642-11486-1_14
28. Lange, T., Neuhäußer, M.R., Noll, T.: IC3 software model checking on control flow
automata. In: Proc. FMCAD. pp. 97–104 (2015)
29. Lange, T., Prinz, F., Neuhäußer, M.R., Noll, T., Katoen, J.: Improving generalization
in software IC3. In: Proc. SPIN’18. pp. 85–102. LNCS 10869, Springer (2018).
https://doi.org/10.1007/978-3-319-94111-0_5
30. McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. CAV. pp.
1–13. LNCS 2725, Springer (2003). https://doi.org/10.1007/978-3-540-45069-6_1
31. Myers, G.J., Sandler, C., Badgett, T.: The Art of Software Testing. Wiley Publishing,
3rd edn. (2011)
32. Wahl, T.: The k-induction principle (2013), available at http://www.ccs.neu.edu/
home/wahl/Publications/k-induction.pdf