Papers that have been read and to be read recently.

[1] Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of Trace Abstraction. SAS 2009: 69-85 (2009). https://doi.org/10.1007/978-3-642-03237-0_7

[2] Rafael Menezes, Herbert Rocha, Lucas C. Cordeiro, Raimundo S. Barreto.: Map2Check Using LLVM and KLEE - (Competition Contribution). TACAS (2) 2018: 437-441 (2018). https://doi.org/10.1007/978-3-319-89963-3_28

[3] F. He, Q. Yu and L. Cai, "Efficient Summary Reuse for Software Regression Verification," in IEEE Transactions on Software Engineering, 2020. Early Access. https://doi.org/10.1109/TSE.2020.3021477.

[4] Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination Analysis by Learning Terminating Programs. In Proceedings of 26th International Conference on Computer Aided Verification (CAV’14). Springer-Verlag New York, Inc., New York, NY, USA, 797–813. https://doi.org/10.1007/978-3-319-08867-9_53

[5] Daca P., Henzinger T.A., Kupriyanov A. (2016) Array Folds Logic. In: Chaudhuri S., Farzan A. (eds) Computer Aided Verification. CAV 2016. Lecture Notes in Computer Science, vol 9780. Springer, Cham. https://doi.org/10.1007/978-3-319-41540-6_13

[6] Chalupa M. (2020) DG: Analysis and Slicing of LLVM Bitcode. In: Hung D.V., Sokolsky O. (eds) Automated Technology for Verification and Analysis. ATVA 2020. Lecture Notes in Computer Science, vol 12302. Springer, Cham. https://doi.org/10.1007/978-3-030-59152-6_33

[7] Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verificationframework. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification- 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9206, pp.343–361. Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_20, Slides.

[8] Singh G, Püschel M, Vechev M. Fast numerical program analysis with reinforcement learning. [C]//International Conference on Computer Aided Verification (CAV'18). Springer, Cham, 2018: 211-229. https://doi.org/10.1007/978-3-319-96145-3_12, Slides

[9] Singh, G., Püschel, M., Vechev, M.T.: A practical construction for decomposing numerical abstract domains. Proc. ACM Program. Lang.2(POPL), 55:1–55:28 (2018). https://doi.org/10.1145/3158143,https://doi.org/10.1145/31581432

[10] Kim S K, Venet A J, Thakur A V. Deterministic parallel fixpoint computation[J]. Proceedings of the ACM on Programming Languages, 2019, 4(POPL): 1-33. https://arxiv.org/pdf/1909.05951.pdf, https://doi.org/10.1145/3371082

[1] Cadar, C., Dunbar, D., Engler, D.R. : KLEE: unassisted and automatic generation of high-converage tests for complex systems programs. In: Draves, R., Van Renesse, R.(eds.) 8th usenix Symposium on Operating Systems Desigh and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. pp.209-224. USENIX Association (2008). http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf

[2] Kapus, T., Ish-Shalom, O., Itzhaky, S., Rinetzky, N., Cadar, C.: Computing summaries of string loops in C for better testing and refactoring. In: McKinley, K.S.,Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Program-ming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June22-26, 2019. pp. 874–888. ACM (2019). https://doi.org/10.1145/3314221.3314610.

[1] Babiak, T., Kretínský, M., Rehák, V., Strejcek, J.: LTL to büchi automatatranslation: Fast and more deterministic. In: Flanagan, C., König, B. (eds.)Tools and Algorithms for the Construction and Analysis of Systems - 18th In-ternational Conference, TACAS 2012. Proceedings. Lecture Notes in Computer Science,vol. 7214, pp. 95–109. Springer (2012). https://doi.org/10.1007/978-3-642-28756-5_8, Slides

[2] Li, Y., Vardi, M.Y., Zhang, L.: On the power of unambiguity in büchi comple-mentation. In: Raskin, J., Bresolin, D. (eds.) Proceedings 11th International Sym-posium on Games, Automata, Logics, and Formal Verification, GandALF 2020,Brussels, Belgium, September 21-22, 2020. EPTCS, vol. 326, pp. 182–198 (2020).https://doi.org/10.4204/EPTCS.326.12.

[3] Blahoudek, F., Heizmann, M., Schewe, S., Strejcek, J., Tsai, M.: Complementing semi-deterministic büchi automata. In: Chechik, M., Raskin, J. (eds.) Toolsand Algorithms for the Construction and Analysis of Systems - 22nd Interna-tional Conference, TACAS 2016, Held as Part of the European Joint Conferenceson Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands,April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9636, pp.770–787. Springer (2016). https://doi.org/10.1007/978-3-662-49674-9_49.

[1] Maler, O., Pnueli, A.: On the learnability of infinitary regular sets. Inf. Com-put.118(2), 316–326 (1995). https://doi.org/10.1006/inco.1995.1070

[1] Carr, S., Jansen, N., Wimmer, R., Serban, A.C., Becker, B., Topcu, U.: Counterexample-guided strategy improvement for pomdps using recurrent neural networks. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth InternationalJoint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019. pp. 5532–5539. ijcai.org (2019). https://doi.org/10.24963/ijcai.2019/768 , Slides

[2] Pineau, J., Gordon, G.J., Thrun, S.: Point-based value iteration: An anytimealgorithm for pomdps. In: Gottlob, G., Walsh, T. (eds.) IJCAI-03, Proceed-ings of the Eighteenth International Joint Conference on Artificial Intelligence,Acapulco, Mexico, August 9-15, 2003. pp. 1025–1032. Morgan Kaufmann (2003). http://ijcai.org/Proceedings/03/Papers/147.pdf

[1] Armstrong, A., Bauereiss, T., Campbell, B., Reid, A., Gray, K.E., Norton, R.M.,Mundkur, P., Wassell, M., French, J., Pulte, C., Flur, S., Stark, I., Krishnaswami,N., Sewell, P.: ISA semantics for armv8-a, risc-v, and CHERI-MIPS. Proc. ACMProgram. Lang.3(POPL), 71:1–71:31 (2019). https://doi.org/10.1145/3290384

[2] Mann, M., Irfan, A., Lonsing, F., Yang, Y., Zhang, H., Brown, K., Gupta, A., Barrett, C.W.: Pono: A flexible and extensible smt-based model checker. CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12760, pp. 461–474. Springer (2021). https://doi.org/10.1007/978-3-030-81688-9_22